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

Theorem dfac5lem4 9540
Description: Lemma for dfac5 9542. (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 3495 . . . . . 6 𝑧 ∈ V
2 neeq1 3075 . . . . . . 7 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3 eqeq1 2822 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
43rexbidv 3294 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
52, 4anbi12d 630 . . . . . 6 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡))))
61, 5elab 3664 . . . . 5 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
76simplbi 498 . . . 4 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
97, 8eleq2s 2928 . . 3 (𝑧𝐴𝑧 ≠ ∅)
109rgen 3145 . 2 𝑧𝐴 𝑧 ≠ ∅
11 df-an 397 . . . . . . 7 ((𝑥𝑧𝑥𝑤) ↔ ¬ (𝑥𝑧 → ¬ 𝑥𝑤))
121, 5, 8elab2 3667 . . . . . . . . 9 (𝑧𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
1312simprbi 497 . . . . . . . 8 (𝑧𝐴 → ∃𝑡 𝑧 = ({𝑡} × 𝑡))
14 vex 3495 . . . . . . . . . . 11 𝑤 ∈ V
15 neeq1 3075 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16 eqeq1 2822 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
1716rexbidv 3294 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
1815, 17anbi12d 630 . . . . . . . . . . 11 (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡))))
1914, 18, 8elab2 3667 . . . . . . . . . 10 (𝑤𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
2019simprbi 497 . . . . . . . . 9 (𝑤𝐴 → ∃𝑡 𝑤 = ({𝑡} × 𝑡))
21 sneq 4567 . . . . . . . . . . . . 13 (𝑡 = 𝑔 → {𝑡} = {𝑔})
2221xpeq1d 5577 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23 xpeq2 5569 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
2422, 23eqtrd 2853 . . . . . . . . . . 11 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
2524eqeq2d 2829 . . . . . . . . . 10 (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
2625cbvrexvw 3448 . . . . . . . . 9 (∃𝑡 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 𝑤 = ({𝑔} × 𝑔))
2720, 26sylib 219 . . . . . . . 8 (𝑤𝐴 → ∃𝑔 𝑤 = ({𝑔} × 𝑔))
28 eleq2 2898 . . . . . . . . . . . . . . . . . 18 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧𝑥 ∈ ({𝑡} × 𝑡)))
29 elxp 5571 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
30 excom 2159 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3129, 30bitri 276 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3228, 31syl6bb 288 . . . . . . . . . . . . . . . . 17 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧 ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡))))
33 eleq2 2898 . . . . . . . . . . . . . . . . . 18 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤𝑥 ∈ ({𝑔} × 𝑔)))
34 elxp 5571 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
35 excom 2159 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3634, 35bitri 276 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3733, 36syl6bb 288 . . . . . . . . . . . . . . . . 17 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤 ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
3832, 37bi2anan9 635 . . . . . . . . . . . . . . . 16 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
39 exdistrv 1947 . . . . . . . . . . . . . . . 16 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
4038, 39syl6bbr 290 . . . . . . . . . . . . . . 15 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ ∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
41 velsn 4573 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
42 opeq1 4795 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
4342eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
4443biimpac 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
4541, 44sylan2b 593 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
4645adantrr 713 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
4746exlimiv 1922 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
48 velsn 4573 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
49 opeq1 4795 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
5049eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
5150biimpac 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
5248, 51sylan2b 593 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
5352adantrr 713 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5453exlimiv 1922 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5547, 54sylan9req 2874 . . . . . . . . . . . . . . . . 17 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
56 vex 3495 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ V
57 vex 3495 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
5856, 57opth1 5358 . . . . . . . . . . . . . . . . 17 (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
5955, 58syl 17 . . . . . . . . . . . . . . . 16 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6059exlimivv 1924 . . . . . . . . . . . . . . 15 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6140, 60syl6bi 254 . . . . . . . . . . . . . 14 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑡 = 𝑔))
6261, 24syl6 35 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
63 eqeq12 2832 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
6462, 63sylibrd 260 . . . . . . . . . . . 12 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6564ex 413 . . . . . . . . . . 11 (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6665rexlimivw 3279 . . . . . . . . . 10 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6766rexlimdvw 3287 . . . . . . . . 9 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6867imp 407 . . . . . . . 8 ((∃𝑡 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6913, 27, 68syl2an 595 . . . . . . 7 ((𝑧𝐴𝑤𝐴) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
7011, 69syl5bir 244 . . . . . 6 ((𝑧𝐴𝑤𝐴) → (¬ (𝑥𝑧 → ¬ 𝑥𝑤) → 𝑧 = 𝑤))
7170necon1ad 3030 . . . . 5 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑥𝑧 → ¬ 𝑥𝑤)))
7271alrimdv 1921 . . . 4 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤)))
73 disj1 4397 . . . 4 ((𝑧𝑤) = ∅ ↔ ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤))
7472, 73syl6ibr 253 . . 3 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑧𝑤) = ∅))
7574rgen2 3200 . 2 𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)
76 dfac5lem.3 . . 3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
77 vex 3495 . . . . . . . 8 ∈ V
78 vuniex 7455 . . . . . . . 8 ∈ V
7977, 78xpex 7465 . . . . . . 7 ( × ) ∈ V
8079pwex 5272 . . . . . 6 𝒫 ( × ) ∈ V
81 snssi 4733 . . . . . . . . . . . 12 (𝑡 → {𝑡} ⊆ )
82 elssuni 4859 . . . . . . . . . . . 12 (𝑡𝑡 )
83 xpss12 5563 . . . . . . . . . . . 12 (({𝑡} ⊆ 𝑡 ) → ({𝑡} × 𝑡) ⊆ ( × ))
8481, 82, 83syl2anc 584 . . . . . . . . . . 11 (𝑡 → ({𝑡} × 𝑡) ⊆ ( × ))
85 snex 5322 . . . . . . . . . . . . 13 {𝑡} ∈ V
8685, 56xpex 7465 . . . . . . . . . . . 12 ({𝑡} × 𝑡) ∈ V
8786elpw 4542 . . . . . . . . . . 11 (({𝑡} × 𝑡) ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ⊆ ( × ))
8884, 87sylibr 235 . . . . . . . . . 10 (𝑡 → ({𝑡} × 𝑡) ∈ 𝒫 ( × ))
89 eleq1 2897 . . . . . . . . . 10 (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 ( × )))
9088, 89syl5ibrcom 248 . . . . . . . . 9 (𝑡 → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × )))
9190rexlimiv 3277 . . . . . . . 8 (∃𝑡 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × ))
9291adantl 482 . . . . . . 7 ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 ( × ))
9392abssi 4043 . . . . . 6 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 ( × )
9480, 93ssexi 5217 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∈ V
958, 94eqeltri 2906 . . . 4 𝐴 ∈ V
96 raleq 3403 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧𝐴 𝑧 ≠ ∅))
97 raleq 3403 . . . . . . 7 (𝑥 = 𝐴 → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9897raleqbi1dv 3401 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9996, 98anbi12d 630 . . . . 5 (𝑥 = 𝐴 → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅))))
100 raleq 3403 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
101100exbidv 1913 . . . . 5 (𝑥 = 𝐴 → (∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10299, 101imbi12d 346 . . . 4 (𝑥 = 𝐴 → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
10395, 102spcv 3603 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10476, 103sylbi 218 . 2 (𝜑 → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10510, 75, 104mp2ani 694 1 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wex 1771  wcel 2105  ∃!weu 2646  {cab 2796  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557  cop 4563   cuni 4830   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  dfac5lem5  9541
  Copyright terms: Public domain W3C validator