Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac5lem4 Structured version   Visualization version   GIF version

Theorem dfac5lem4 8987
 Description: Lemma for dfac5 8989. (Contributed by NM, 11-Apr-2004.)
Hypotheses
Ref Expression
dfac5lem.1 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
dfac5lem.2 𝐵 = ( 𝐴𝑦)
dfac5lem.3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
Assertion
Ref Expression
dfac5lem4 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Distinct variable groups:   𝑥,𝑧,𝑦,𝑤,𝑣,𝑢,𝑡,   𝑧,𝐵,𝑤   𝑥,𝐴,𝑦,𝑧,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑡,)   𝐴(𝑣,𝑢,𝑡,)   𝐵(𝑥,𝑦,𝑣,𝑢,𝑡,)

Proof of Theorem dfac5lem4
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 vex 3234 . . . . . 6 𝑧 ∈ V
2 neeq1 2885 . . . . . . 7 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3 eqeq1 2655 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
43rexbidv 3081 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
52, 4anbi12d 747 . . . . . 6 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡))))
61, 5elab 3382 . . . . 5 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
76simplbi 475 . . . 4 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
97, 8eleq2s 2748 . . 3 (𝑧𝐴𝑧 ≠ ∅)
109rgen 2951 . 2 𝑧𝐴 𝑧 ≠ ∅
11 df-an 385 . . . . . . 7 ((𝑥𝑧𝑥𝑤) ↔ ¬ (𝑥𝑧 → ¬ 𝑥𝑤))
121, 5, 8elab2 3386 . . . . . . . . 9 (𝑧𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
1312simprbi 479 . . . . . . . 8 (𝑧𝐴 → ∃𝑡 𝑧 = ({𝑡} × 𝑡))
14 vex 3234 . . . . . . . . . . 11 𝑤 ∈ V
15 neeq1 2885 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16 eqeq1 2655 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
1716rexbidv 3081 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
1815, 17anbi12d 747 . . . . . . . . . . 11 (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡))))
1914, 18, 8elab2 3386 . . . . . . . . . 10 (𝑤𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
2019simprbi 479 . . . . . . . . 9 (𝑤𝐴 → ∃𝑡 𝑤 = ({𝑡} × 𝑡))
21 sneq 4220 . . . . . . . . . . . . 13 (𝑡 = 𝑔 → {𝑡} = {𝑔})
2221xpeq1d 5172 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23 xpeq2 5163 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
2422, 23eqtrd 2685 . . . . . . . . . . 11 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
2524eqeq2d 2661 . . . . . . . . . 10 (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
2625cbvrexv 3202 . . . . . . . . 9 (∃𝑡 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 𝑤 = ({𝑔} × 𝑔))
2720, 26sylib 208 . . . . . . . 8 (𝑤𝐴 → ∃𝑔 𝑤 = ({𝑔} × 𝑔))
28 eleq2 2719 . . . . . . . . . . . . . . . . . 18 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧𝑥 ∈ ({𝑡} × 𝑡)))
29 elxp 5165 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
30 excom 2082 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3129, 30bitri 264 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3228, 31syl6bb 276 . . . . . . . . . . . . . . . . 17 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧 ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡))))
33 eleq2 2719 . . . . . . . . . . . . . . . . . 18 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤𝑥 ∈ ({𝑔} × 𝑔)))
34 elxp 5165 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
35 excom 2082 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3634, 35bitri 264 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3733, 36syl6bb 276 . . . . . . . . . . . . . . . . 17 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤 ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
3832, 37bi2anan9 935 . . . . . . . . . . . . . . . 16 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
39 eeanv 2218 . . . . . . . . . . . . . . . 16 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
4038, 39syl6bbr 278 . . . . . . . . . . . . . . 15 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ ∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
41 velsn 4226 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
42 opeq1 4433 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
4342eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
4443biimpac 502 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
4541, 44sylan2b 491 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
4645adantrr 753 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
4746exlimiv 1898 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
48 velsn 4226 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
49 opeq1 4433 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
5049eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
5150biimpac 502 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
5248, 51sylan2b 491 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
5352adantrr 753 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5453exlimiv 1898 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5547, 54sylan9req 2706 . . . . . . . . . . . . . . . . 17 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
56 vex 3234 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ V
57 vex 3234 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
5856, 57opth1 4973 . . . . . . . . . . . . . . . . 17 (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
5955, 58syl 17 . . . . . . . . . . . . . . . 16 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6059exlimivv 1900 . . . . . . . . . . . . . . 15 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6140, 60syl6bi 243 . . . . . . . . . . . . . 14 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑡 = 𝑔))
6261, 24syl6 35 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
63 eqeq12 2664 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
6462, 63sylibrd 249 . . . . . . . . . . . 12 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6564ex 449 . . . . . . . . . . 11 (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6665rexlimivw 3058 . . . . . . . . . 10 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6766rexlimdvw 3063 . . . . . . . . 9 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6867imp 444 . . . . . . . 8 ((∃𝑡 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6913, 27, 68syl2an 493 . . . . . . 7 ((𝑧𝐴𝑤𝐴) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
7011, 69syl5bir 233 . . . . . 6 ((𝑧𝐴𝑤𝐴) → (¬ (𝑥𝑧 → ¬ 𝑥𝑤) → 𝑧 = 𝑤))
7170necon1ad 2840 . . . . 5 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑥𝑧 → ¬ 𝑥𝑤)))
7271alrimdv 1897 . . . 4 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤)))
73 disj1 4052 . . . 4 ((𝑧𝑤) = ∅ ↔ ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤))
7472, 73syl6ibr 242 . . 3 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑧𝑤) = ∅))
7574rgen2a 3006 . 2 𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)
76 dfac5lem.3 . . 3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
77 vex 3234 . . . . . . . 8 ∈ V
78 vuniex 6996 . . . . . . . 8 ∈ V
7977, 78xpex 7004 . . . . . . 7 ( × ) ∈ V
8079pwex 4878 . . . . . 6 𝒫 ( × ) ∈ V
81 snssi 4371 . . . . . . . . . . . 12 (𝑡 → {𝑡} ⊆ )
82 elssuni 4499 . . . . . . . . . . . 12 (𝑡𝑡 )
83 xpss12 5158 . . . . . . . . . . . 12 (({𝑡} ⊆ 𝑡 ) → ({𝑡} × 𝑡) ⊆ ( × ))
8481, 82, 83syl2anc 694 . . . . . . . . . . 11 (𝑡 → ({𝑡} × 𝑡) ⊆ ( × ))
85 snex 4938 . . . . . . . . . . . . 13 {𝑡} ∈ V
8685, 56xpex 7004 . . . . . . . . . . . 12 ({𝑡} × 𝑡) ∈ V
8786elpw 4197 . . . . . . . . . . 11 (({𝑡} × 𝑡) ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ⊆ ( × ))
8884, 87sylibr 224 . . . . . . . . . 10 (𝑡 → ({𝑡} × 𝑡) ∈ 𝒫 ( × ))
89 eleq1 2718 . . . . . . . . . 10 (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 ( × )))
9088, 89syl5ibrcom 237 . . . . . . . . 9 (𝑡 → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × )))
9190rexlimiv 3056 . . . . . . . 8 (∃𝑡 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × ))
9291adantl 481 . . . . . . 7 ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 ( × ))
9392abssi 3710 . . . . . 6 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 ( × )
9480, 93ssexi 4836 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∈ V
958, 94eqeltri 2726 . . . 4 𝐴 ∈ V
96 raleq 3168 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧𝐴 𝑧 ≠ ∅))
97 raleq 3168 . . . . . . 7 (𝑥 = 𝐴 → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9897raleqbi1dv 3176 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9996, 98anbi12d 747 . . . . 5 (𝑥 = 𝐴 → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅))))
100 raleq 3168 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
101100exbidv 1890 . . . . 5 (𝑥 = 𝐴 → (∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10299, 101imbi12d 333 . . . 4 (𝑥 = 𝐴 → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
10395, 102spcv 3330 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10476, 103sylbi 207 . 2 (𝜑 → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10510, 75, 104mp2ani 714 1 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∃!weu 2498  {cab 2637   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  {csn 4210  ⟨cop 4216  ∪ cuni 4468   × cxp 5141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-opab 4746  df-xp 5149  df-rel 5150 This theorem is referenced by:  dfac5lem5  8988
 Copyright terms: Public domain W3C validator