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

Theorem dfac5lem4 8900
Description: Lemma for dfac5 8902. (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 3192 . . . . . 6 𝑧 ∈ V
2 neeq1 2852 . . . . . . 7 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
3 eqeq1 2625 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡)))
43rexbidv 3046 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
52, 4anbi12d 746 . . . . . 6 (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡))))
61, 5elab 3337 . . . . 5 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
76simplbi 476 . . . 4 (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅)
8 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
97, 8eleq2s 2716 . . 3 (𝑧𝐴𝑧 ≠ ∅)
109rgen 2917 . 2 𝑧𝐴 𝑧 ≠ ∅
11 df-an 386 . . . . . . 7 ((𝑥𝑧𝑥𝑤) ↔ ¬ (𝑥𝑧 → ¬ 𝑥𝑤))
121, 5, 8elab2 3341 . . . . . . . . 9 (𝑧𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 𝑧 = ({𝑡} × 𝑡)))
1312simprbi 480 . . . . . . . 8 (𝑧𝐴 → ∃𝑡 𝑧 = ({𝑡} × 𝑡))
14 vex 3192 . . . . . . . . . . 11 𝑤 ∈ V
15 neeq1 2852 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅))
16 eqeq1 2625 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡)))
1716rexbidv 3046 . . . . . . . . . . . 12 (𝑢 = 𝑤 → (∃𝑡 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
1815, 17anbi12d 746 . . . . . . . . . . 11 (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡))))
1914, 18, 8elab2 3341 . . . . . . . . . 10 (𝑤𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 𝑤 = ({𝑡} × 𝑡)))
2019simprbi 480 . . . . . . . . 9 (𝑤𝐴 → ∃𝑡 𝑤 = ({𝑡} × 𝑡))
21 sneq 4163 . . . . . . . . . . . . 13 (𝑡 = 𝑔 → {𝑡} = {𝑔})
2221xpeq1d 5103 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡))
23 xpeq2 5094 . . . . . . . . . . . 12 (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔))
2422, 23eqtrd 2655 . . . . . . . . . . 11 (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))
2524eqeq2d 2631 . . . . . . . . . 10 (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔)))
2625cbvrexv 3163 . . . . . . . . 9 (∃𝑡 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 𝑤 = ({𝑔} × 𝑔))
2720, 26sylib 208 . . . . . . . 8 (𝑤𝐴 → ∃𝑔 𝑤 = ({𝑔} × 𝑔))
28 eleq2 2687 . . . . . . . . . . . . . . . . . 18 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧𝑥 ∈ ({𝑡} × 𝑡)))
29 elxp 5096 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
30 excom 2039 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3129, 30bitri 264 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)))
3228, 31syl6bb 276 . . . . . . . . . . . . . . . . 17 (𝑧 = ({𝑡} × 𝑡) → (𝑥𝑧 ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡))))
33 eleq2 2687 . . . . . . . . . . . . . . . . . 18 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤𝑥 ∈ ({𝑔} × 𝑔)))
34 elxp 5096 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
35 excom 2039 . . . . . . . . . . . . . . . . . . 19 (∃𝑢𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3634, 35bitri 264 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))
3733, 36syl6bb 276 . . . . . . . . . . . . . . . . 17 (𝑤 = ({𝑔} × 𝑔) → (𝑥𝑤 ↔ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
3832, 37bi2anan9 916 . . . . . . . . . . . . . . . 16 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
39 eeanv 2181 . . . . . . . . . . . . . . . 16 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) ↔ (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑦𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))))
4038, 39syl6bbr 278 . . . . . . . . . . . . . . 15 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) ↔ ∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)))))
41 velsn 4169 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡)
42 opeq1 4375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩)
4342eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩))
4443biimpac 503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩)
4541, 44sylan2b 492 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩)
4645adantrr 752 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
4746exlimiv 1855 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩)
48 velsn 4169 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔)
49 opeq1 4375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩)
5049eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩))
5150biimpac 503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩)
5248, 51sylan2b 492 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩)
5352adantrr 752 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5453exlimiv 1855 . . . . . . . . . . . . . . . . . 18 (∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩)
5547, 54sylan9req 2676 . . . . . . . . . . . . . . . . 17 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩)
56 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ V
57 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
5856, 57opth1 4909 . . . . . . . . . . . . . . . . 17 (⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔)
5955, 58syl 17 . . . . . . . . . . . . . . . 16 ((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6059exlimivv 1857 . . . . . . . . . . . . . . 15 (∃𝑣𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦𝑔))) → 𝑡 = 𝑔)
6140, 60syl6bi 243 . . . . . . . . . . . . . 14 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑡 = 𝑔))
6261, 24syl6 35 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
63 eqeq12 2634 . . . . . . . . . . . . 13 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔)))
6462, 63sylibrd 249 . . . . . . . . . . . 12 ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6564ex 450 . . . . . . . . . . 11 (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6665rexlimivw 3023 . . . . . . . . . 10 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6766rexlimdvw 3028 . . . . . . . . 9 (∃𝑡 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 𝑤 = ({𝑔} × 𝑔) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤)))
6867imp 445 . . . . . . . 8 ((∃𝑡 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 𝑤 = ({𝑔} × 𝑔)) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
6913, 27, 68syl2an 494 . . . . . . 7 ((𝑧𝐴𝑤𝐴) → ((𝑥𝑧𝑥𝑤) → 𝑧 = 𝑤))
7011, 69syl5bir 233 . . . . . 6 ((𝑧𝐴𝑤𝐴) → (¬ (𝑥𝑧 → ¬ 𝑥𝑤) → 𝑧 = 𝑤))
7170necon1ad 2807 . . . . 5 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑥𝑧 → ¬ 𝑥𝑤)))
7271alrimdv 1854 . . . 4 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤)))
73 disj1 3996 . . . 4 ((𝑧𝑤) = ∅ ↔ ∀𝑥(𝑥𝑧 → ¬ 𝑥𝑤))
7472, 73syl6ibr 242 . . 3 ((𝑧𝐴𝑤𝐴) → (𝑧𝑤 → (𝑧𝑤) = ∅))
7574rgen2a 2972 . 2 𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)
76 dfac5lem.3 . . 3 (𝜑 ↔ ∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
77 vex 3192 . . . . . . . 8 ∈ V
78 vuniex 6914 . . . . . . . 8 ∈ V
7977, 78xpex 6922 . . . . . . 7 ( × ) ∈ V
8079pwex 4813 . . . . . 6 𝒫 ( × ) ∈ V
81 snssi 4313 . . . . . . . . . . . 12 (𝑡 → {𝑡} ⊆ )
82 elssuni 4438 . . . . . . . . . . . 12 (𝑡𝑡 )
83 xpss12 5191 . . . . . . . . . . . 12 (({𝑡} ⊆ 𝑡 ) → ({𝑡} × 𝑡) ⊆ ( × ))
8481, 82, 83syl2anc 692 . . . . . . . . . . 11 (𝑡 → ({𝑡} × 𝑡) ⊆ ( × ))
85 snex 4874 . . . . . . . . . . . . 13 {𝑡} ∈ V
8685, 56xpex 6922 . . . . . . . . . . . 12 ({𝑡} × 𝑡) ∈ V
8786elpw 4141 . . . . . . . . . . 11 (({𝑡} × 𝑡) ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ⊆ ( × ))
8884, 87sylibr 224 . . . . . . . . . 10 (𝑡 → ({𝑡} × 𝑡) ∈ 𝒫 ( × ))
89 eleq1 2686 . . . . . . . . . 10 (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 ( × ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 ( × )))
9088, 89syl5ibrcom 237 . . . . . . . . 9 (𝑡 → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × )))
9190rexlimiv 3021 . . . . . . . 8 (∃𝑡 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 ( × ))
9291adantl 482 . . . . . . 7 ((𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 ( × ))
9392abssi 3661 . . . . . 6 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 ( × )
9480, 93ssexi 4768 . . . . 5 {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ∈ V
958, 94eqeltri 2694 . . . 4 𝐴 ∈ V
96 raleq 3130 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧𝐴 𝑧 ≠ ∅))
97 raleq 3130 . . . . . . 7 (𝑥 = 𝐴 → (∀𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9897raleqbi1dv 3138 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)))
9996, 98anbi12d 746 . . . . 5 (𝑥 = 𝐴 → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) ↔ (∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅))))
100 raleq 3130 . . . . . 6 (𝑥 = 𝐴 → (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
101100exbidv 1847 . . . . 5 (𝑥 = 𝐴 → (∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10299, 101imbi12d 334 . . . 4 (𝑥 = 𝐴 → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
10395, 102spcv 3288 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10476, 103sylbi 207 . 2 (𝜑 → ((∀𝑧𝐴 𝑧 ≠ ∅ ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤 → (𝑧𝑤) = ∅)) → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
10510, 75, 104mp2ani 713 1 (𝜑 → ∃𝑦𝑧𝐴 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  ∃!weu 2469  {cab 2607  wne 2790  wral 2907  wrex 2908  Vcvv 3189  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153  cop 4159   cuni 4407   × cxp 5077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-opab 4679  df-xp 5085  df-rel 5086
This theorem is referenced by:  dfac5lem5  8901
  Copyright terms: Public domain W3C validator