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

Theorem dfac5lem4 10070
Description: Lemma for dfac5 10072. (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 3451 . . . . . 6 𝑧 ∈ V
2 neeq1 3003 . . . . . . 7 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3 eqeq1 2737 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
43rexbidv 3172 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
52, 4anbi12d 632 . . . . . 6 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡))))
61, 5elab 3634 . . . . 5 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
76simplbi 499 . . . 4 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
97, 8eleq2s 2852 . . 3 (𝑧𝐴𝑧 ≠ ∅)
109rgen 3063 . 2 𝑧𝐴 𝑧 ≠ ∅
11 df-an 398 . . . . . . 7 ((𝑥𝑧𝑥𝑤) ↔ ¬ (𝑥𝑧 → ¬ 𝑥𝑤))
121, 5, 8elab2 3638 . . . . . . . . 9 (𝑧𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
1312simprbi 498 . . . . . . . 8 (𝑧𝐴 → ∃𝑡 𝑧 = ({𝑡} × 𝑡))
14 vex 3451 . . . . . . . . . . 11 𝑤 ∈ V
15 neeq1 3003 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16 eqeq1 2737 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
1716rexbidv 3172 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
1815, 17anbi12d 632 . . . . . . . . . . 11 (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡))))
1914, 18, 8elab2 3638 . . . . . . . . . 10 (𝑤𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
2019simprbi 498 . . . . . . . . 9 (𝑤𝐴 → ∃𝑡 𝑤 = ({𝑡} × 𝑡))
21 sneq 4600 . . . . . . . . . . . . 13 (𝑡 = 𝑔 → {𝑡} = {𝑔})
2221xpeq1d 5666 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23 xpeq2 5658 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
2422, 23eqtrd 2773 . . . . . . . . . . 11 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
2524eqeq2d 2744 . . . . . . . . . 10 (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
2625cbvrexvw 3225 . . . . . . . . 9 (∃𝑡 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 𝑤 = ({𝑔} × 𝑔))
2720, 26sylib 217 . . . . . . . 8 (𝑤𝐴 → ∃𝑔 𝑤 = ({𝑔} × 𝑔))
28 eleq2 2823 . . . . . . . . . . . . . . . . . 18 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧𝑥 ∈ ({𝑡} × 𝑡)))
29 elxp 5660 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
30 excom 2163 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3129, 30bitri 275 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3228, 31bitrdi 287 . . . . . . . . . . . . . . . . 17 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧 ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡))))
33 eleq2 2823 . . . . . . . . . . . . . . . . . 18 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤𝑥 ∈ ({𝑔} × 𝑔)))
34 elxp 5660 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
35 excom 2163 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3634, 35bitri 275 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3733, 36bitrdi 287 . . . . . . . . . . . . . . . . 17 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤 ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
3832, 37bi2anan9 638 . . . . . . . . . . . . . . . 16 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
39 exdistrv 1960 . . . . . . . . . . . . . . . 16 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
4038, 39bitr4di 289 . . . . . . . . . . . . . . 15 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ ∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
41 velsn 4606 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
42 opeq1 4834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
4342eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
4443biimpac 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
4541, 44sylan2b 595 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
4645adantrr 716 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
4746exlimiv 1934 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
48 velsn 4606 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
49 opeq1 4834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
5049eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
5150biimpac 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
5248, 51sylan2b 595 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
5352adantrr 716 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5453exlimiv 1934 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5547, 54sylan9req 2794 . . . . . . . . . . . . . . . . 17 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
56 vex 3451 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ V
57 vex 3451 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
5856, 57opth1 5436 . . . . . . . . . . . . . . . . 17 (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
5955, 58syl 17 . . . . . . . . . . . . . . . 16 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6059exlimivv 1936 . . . . . . . . . . . . . . 15 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6140, 60syl6bi 253 . . . . . . . . . . . . . 14 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑡 = 𝑔))
6261, 24syl6 35 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
63 eqeq12 2750 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
6462, 63sylibrd 259 . . . . . . . . . . . 12 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6564ex 414 . . . . . . . . . . 11 (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6665rexlimivw 3145 . . . . . . . . . 10 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6766rexlimdvw 3154 . . . . . . . . 9 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6867imp 408 . . . . . . . 8 ((∃𝑡 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6913, 27, 68syl2an 597 . . . . . . 7 ((𝑧𝐴𝑤𝐴) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
7011, 69biimtrrid 242 . . . . . 6 ((𝑧𝐴𝑤𝐴) → (¬ (𝑥𝑧 → ¬ 𝑥𝑤) → 𝑧 = 𝑤))
7170necon1ad 2957 . . . . 5 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑥𝑧 → ¬ 𝑥𝑤)))
7271alrimdv 1933 . . . 4 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤)))
73 disj1 4414 . . . 4 ((𝑧𝑤) = ∅ ↔ ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤))
7472, 73syl6ibr 252 . . 3 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑧𝑤) = ∅))
7574rgen2 3191 . 2 𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)
76 dfac5lem.3 . . 3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
77 vex 3451 . . . . . . . 8 ∈ V
78 vuniex 7680 . . . . . . . 8 ∈ V
7977, 78xpex 7691 . . . . . . 7 ( × ) ∈ V
8079pwex 5339 . . . . . 6 𝒫 ( × ) ∈ V
81 snssi 4772 . . . . . . . . . . . 12 (𝑡 → {𝑡} ⊆ )
82 elssuni 4902 . . . . . . . . . . . 12 (𝑡𝑡 )
83 xpss12 5652 . . . . . . . . . . . 12 (({𝑡} ⊆ 𝑡 ) → ({𝑡} × 𝑡) ⊆ ( × ))
8481, 82, 83syl2anc 585 . . . . . . . . . . 11 (𝑡 → ({𝑡} × 𝑡) ⊆ ( × ))
85 vsnex 5390 . . . . . . . . . . . . 13 {𝑡} ∈ V
8685, 56xpex 7691 . . . . . . . . . . . 12 ({𝑡} × 𝑡) ∈ V
8786elpw 4568 . . . . . . . . . . 11 (({𝑡} × 𝑡) ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ⊆ ( × ))
8884, 87sylibr 233 . . . . . . . . . 10 (𝑡 → ({𝑡} × 𝑡) ∈ 𝒫 ( × ))
89 eleq1 2822 . . . . . . . . . 10 (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 ( × )))
9088, 89syl5ibrcom 247 . . . . . . . . 9 (𝑡 → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × )))
9190rexlimiv 3142 . . . . . . . 8 (∃𝑡 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × ))
9291adantl 483 . . . . . . 7 ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 ( × ))
9392abssi 4031 . . . . . 6 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 ( × )
9480, 93ssexi 5283 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∈ V
958, 94eqeltri 2830 . . . 4 𝐴 ∈ V
96 raleq 3308 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧𝐴 𝑧 ≠ ∅))
97 raleq 3308 . . . . . . 7 (𝑥 = 𝐴 → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9897raleqbi1dv 3306 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9996, 98anbi12d 632 . . . . 5 (𝑥 = 𝐴 → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅))))
100 raleq 3308 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
101100exbidv 1925 . . . . 5 (𝑥 = 𝐴 → (∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10299, 101imbi12d 345 . . . 4 (𝑥 = 𝐴 → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
10395, 102spcv 3566 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10476, 103sylbi 216 . 2 (𝜑 → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10510, 75, 104mp2ani 697 1 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  ∃!weu 2563  {cab 2710  wne 2940  wral 3061  wrex 3070  Vcvv 3447  cin 3913  wss 3914  c0 4286  𝒫 cpw 4564  {csn 4590  cop 4596   cuni 4869   × cxp 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-opab 5172  df-xp 5643  df-rel 5644
This theorem is referenced by:  dfac5lem5  10071
  Copyright terms: Public domain W3C validator