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

Theorem dfac5lem4 9241
Description: Lemma for dfac5 9243. (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 3405 . . . . . 6 𝑧 ∈ V
2 neeq1 3051 . . . . . . 7 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3 eqeq1 2821 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
43rexbidv 3251 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
52, 4anbi12d 618 . . . . . 6 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡))))
61, 5elab 3556 . . . . 5 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
76simplbi 487 . . . 4 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
97, 8eleq2s 2914 . . 3 (𝑧𝐴𝑧 ≠ ∅)
109rgen 3121 . 2 𝑧𝐴 𝑧 ≠ ∅
11 df-an 385 . . . . . . 7 ((𝑥𝑧𝑥𝑤) ↔ ¬ (𝑥𝑧 → ¬ 𝑥𝑤))
121, 5, 8elab2 3560 . . . . . . . . 9 (𝑧𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
1312simprbi 486 . . . . . . . 8 (𝑧𝐴 → ∃𝑡 𝑧 = ({𝑡} × 𝑡))
14 vex 3405 . . . . . . . . . . 11 𝑤 ∈ V
15 neeq1 3051 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16 eqeq1 2821 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
1716rexbidv 3251 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
1815, 17anbi12d 618 . . . . . . . . . . 11 (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡))))
1914, 18, 8elab2 3560 . . . . . . . . . 10 (𝑤𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
2019simprbi 486 . . . . . . . . 9 (𝑤𝐴 → ∃𝑡 𝑤 = ({𝑡} × 𝑡))
21 sneq 4391 . . . . . . . . . . . . 13 (𝑡 = 𝑔 → {𝑡} = {𝑔})
2221xpeq1d 5352 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23 xpeq2 5344 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
2422, 23eqtrd 2851 . . . . . . . . . . 11 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
2524eqeq2d 2827 . . . . . . . . . 10 (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
2625cbvrexv 3372 . . . . . . . . 9 (∃𝑡 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 𝑤 = ({𝑔} × 𝑔))
2720, 26sylib 209 . . . . . . . 8 (𝑤𝐴 → ∃𝑔 𝑤 = ({𝑔} × 𝑔))
28 eleq2 2885 . . . . . . . . . . . . . . . . . 18 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧𝑥 ∈ ({𝑡} × 𝑡)))
29 elxp 5346 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
30 excom 2210 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3129, 30bitri 266 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3228, 31syl6bb 278 . . . . . . . . . . . . . . . . 17 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧 ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡))))
33 eleq2 2885 . . . . . . . . . . . . . . . . . 18 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤𝑥 ∈ ({𝑔} × 𝑔)))
34 elxp 5346 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
35 excom 2210 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3634, 35bitri 266 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3733, 36syl6bb 278 . . . . . . . . . . . . . . . . 17 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤 ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
3832, 37bi2anan9 622 . . . . . . . . . . . . . . . 16 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
39 eeanv 2358 . . . . . . . . . . . . . . . 16 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
4038, 39syl6bbr 280 . . . . . . . . . . . . . . 15 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ ∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
41 velsn 4397 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
42 opeq1 4606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
4342eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
4443biimpac 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
4541, 44sylan2b 583 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
4645adantrr 699 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
4746exlimiv 2021 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
48 velsn 4397 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
49 opeq1 4606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
5049eqeq2d 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
5150biimpac 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
5248, 51sylan2b 583 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
5352adantrr 699 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5453exlimiv 2021 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5547, 54sylan9req 2872 . . . . . . . . . . . . . . . . 17 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
56 vex 3405 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ V
57 vex 3405 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
5856, 57opth1 5146 . . . . . . . . . . . . . . . . 17 (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
5955, 58syl 17 . . . . . . . . . . . . . . . 16 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6059exlimivv 2023 . . . . . . . . . . . . . . 15 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6140, 60syl6bi 244 . . . . . . . . . . . . . 14 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑡 = 𝑔))
6261, 24syl6 35 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
63 eqeq12 2830 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
6462, 63sylibrd 250 . . . . . . . . . . . 12 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6564ex 399 . . . . . . . . . . 11 (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6665rexlimivw 3228 . . . . . . . . . 10 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6766rexlimdvw 3233 . . . . . . . . 9 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6867imp 395 . . . . . . . 8 ((∃𝑡 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6913, 27, 68syl2an 585 . . . . . . 7 ((𝑧𝐴𝑤𝐴) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
7011, 69syl5bir 234 . . . . . 6 ((𝑧𝐴𝑤𝐴) → (¬ (𝑥𝑧 → ¬ 𝑥𝑤) → 𝑧 = 𝑤))
7170necon1ad 3006 . . . . 5 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑥𝑧 → ¬ 𝑥𝑤)))
7271alrimdv 2020 . . . 4 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤)))
73 disj1 4227 . . . 4 ((𝑧𝑤) = ∅ ↔ ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤))
7472, 73syl6ibr 243 . . 3 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑧𝑤) = ∅))
7574rgen2a 3176 . 2 𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)
76 dfac5lem.3 . . 3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
77 vex 3405 . . . . . . . 8 ∈ V
78 vuniex 7193 . . . . . . . 8 ∈ V
7977, 78xpex 7201 . . . . . . 7 ( × ) ∈ V
8079pwex 5063 . . . . . 6 𝒫 ( × ) ∈ V
81 snssi 4540 . . . . . . . . . . . 12 (𝑡 → {𝑡} ⊆ )
82 elssuni 4672 . . . . . . . . . . . 12 (𝑡𝑡 )
83 xpss12 5339 . . . . . . . . . . . 12 (({𝑡} ⊆ 𝑡 ) → ({𝑡} × 𝑡) ⊆ ( × ))
8481, 82, 83syl2anc 575 . . . . . . . . . . 11 (𝑡 → ({𝑡} × 𝑡) ⊆ ( × ))
85 snex 5111 . . . . . . . . . . . . 13 {𝑡} ∈ V
8685, 56xpex 7201 . . . . . . . . . . . 12 ({𝑡} × 𝑡) ∈ V
8786elpw 4368 . . . . . . . . . . 11 (({𝑡} × 𝑡) ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ⊆ ( × ))
8884, 87sylibr 225 . . . . . . . . . 10 (𝑡 → ({𝑡} × 𝑡) ∈ 𝒫 ( × ))
89 eleq1 2884 . . . . . . . . . 10 (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 ( × )))
9088, 89syl5ibrcom 238 . . . . . . . . 9 (𝑡 → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × )))
9190rexlimiv 3226 . . . . . . . 8 (∃𝑡 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × ))
9291adantl 469 . . . . . . 7 ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 ( × ))
9392abssi 3885 . . . . . 6 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 ( × )
9480, 93ssexi 5011 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∈ V
958, 94eqeltri 2892 . . . 4 𝐴 ∈ V
96 raleq 3338 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧𝐴 𝑧 ≠ ∅))
97 raleq 3338 . . . . . . 7 (𝑥 = 𝐴 → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9897raleqbi1dv 3346 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9996, 98anbi12d 618 . . . . 5 (𝑥 = 𝐴 → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅))))
100 raleq 3338 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
101100exbidv 2012 . . . . 5 (𝑥 = 𝐴 → (∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10299, 101imbi12d 335 . . . 4 (𝑥 = 𝐴 → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
10395, 102spcv 3503 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10476, 103sylbi 208 . 2 (𝜑 → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10510, 75, 104mp2ani 681 1 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2157  ∃!weu 2641  {cab 2803  wne 2989  wral 3107  wrex 3108  Vcvv 3402  cin 3779  wss 3780  c0 4127  𝒫 cpw 4362  {csn 4381  cop 4387   cuni 4641   × cxp 5322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-opab 4918  df-xp 5330  df-rel 5331
This theorem is referenced by:  dfac5lem5  9242
  Copyright terms: Public domain W3C validator