This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfac5lem4

Description: Lemma for dfac5 . (Contributed by NM, 11-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025)

Ref Expression
Hypotheses dfac5lem.1 ⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
dfac5lem.2 ⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
Assertion dfac5lem4 ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dfac5lem.1 ⊢ 𝐴 = { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) }
2 dfac5lem.2 ⊢ ( 𝜑 ↔ ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
3 vex ⊢ 𝑧 ∈ V
4 neeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
5 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
6 5 rexbidv ⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
7 4 6 anbi12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) ) )
8 3 7 elab ⊢ ( 𝑧 ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
9 8 simplbi ⊢ ( 𝑧 ∈ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } → 𝑧 ≠ ∅ )
10 9 1 eleq2s ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ≠ ∅ )
11 10 rgen ⊢ ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅
12 df-an ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) ↔ ¬ ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) )
13 3 7 1 elab2 ⊢ ( 𝑧 ∈ 𝐴 ↔ ( 𝑧 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ) )
14 13 simprbi ⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) )
15 vex ⊢ 𝑤 ∈ V
16 neeq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅ ) )
17 eqeq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
18 17 rexbidv ⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
19 16 18 anbi12d ⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) ) )
20 15 19 1 elab2 ⊢ ( 𝑤 ∈ 𝐴 ↔ ( 𝑤 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ) )
21 20 simprbi ⊢ ( 𝑤 ∈ 𝐴 → ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) )
22 sneq ⊢ ( 𝑡 = 𝑔 → { 𝑡 } = { 𝑔 } )
23 22 xpeq1d ⊢ ( 𝑡 = 𝑔 → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑡 ) )
24 xpeq2 ⊢ ( 𝑡 = 𝑔 → ( { 𝑔 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) )
25 23 24 eqtrd ⊢ ( 𝑡 = 𝑔 → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) )
26 25 eqeq2d ⊢ ( 𝑡 = 𝑔 → ( 𝑤 = ( { 𝑡 } × 𝑡 ) ↔ 𝑤 = ( { 𝑔 } × 𝑔 ) ) )
27 26 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ℎ 𝑤 = ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) )
28 21 27 sylib ⊢ ( 𝑤 ∈ 𝐴 → ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) )
29 eleq2 ⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( { 𝑡 } × 𝑡 ) ) )
30 elxp ⊢ ( 𝑥 ∈ ( { 𝑡 } × 𝑡 ) ↔ ∃ 𝑢 ∃ 𝑣 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
31 opeq1 ⊢ ( 𝑢 = 𝑠 → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑠 , 𝑣 ⟩ )
32 31 eqeq2d ⊢ ( 𝑢 = 𝑠 → ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ↔ 𝑥 = ⟨ 𝑠 , 𝑣 ⟩ ) )
33 eleq1w ⊢ ( 𝑢 = 𝑠 → ( 𝑢 ∈ { 𝑡 } ↔ 𝑠 ∈ { 𝑡 } ) )
34 33 anbi1d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ↔ ( 𝑠 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
35 32 34 anbi12d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ↔ ( 𝑥 = ⟨ 𝑠 , 𝑣 ⟩ ∧ ( 𝑠 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ) )
36 35 excomimw ⊢ ( ∃ 𝑢 ∃ 𝑣 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
37 30 36 sylbi ⊢ ( 𝑥 ∈ ( { 𝑡 } × 𝑡 ) → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) )
38 29 37 biimtrdi ⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ) )
39 eleq2 ⊢ ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( { 𝑔 } × 𝑔 ) ) )
40 elxp ⊢ ( 𝑥 ∈ ( { 𝑔 } × 𝑔 ) ↔ ∃ 𝑢 ∃ 𝑦 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
41 opeq1 ⊢ ( 𝑢 = 𝑠 → ⟨ 𝑢 , 𝑦 ⟩ = ⟨ 𝑠 , 𝑦 ⟩ )
42 41 eqeq2d ⊢ ( 𝑢 = 𝑠 → ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ↔ 𝑥 = ⟨ 𝑠 , 𝑦 ⟩ ) )
43 eleq1w ⊢ ( 𝑢 = 𝑠 → ( 𝑢 ∈ { 𝑔 } ↔ 𝑠 ∈ { 𝑔 } ) )
44 43 anbi1d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ↔ ( 𝑠 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
45 42 44 anbi12d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ↔ ( 𝑥 = ⟨ 𝑠 , 𝑦 ⟩ ∧ ( 𝑠 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
46 45 excomimw ⊢ ( ∃ 𝑢 ∃ 𝑦 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
47 40 46 sylbi ⊢ ( 𝑥 ∈ ( { 𝑔 } × 𝑔 ) → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) )
48 39 47 biimtrdi ⊢ ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( 𝑥 ∈ 𝑤 → ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
49 38 48 im2anan9 ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ( ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ) )
50 exdistrv ⊢ ( ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ↔ ( ∃ 𝑣 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑦 ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) )
51 49 50 imbitrrdi ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) ) )
52 velsn ⊢ ( 𝑢 ∈ { 𝑡 } ↔ 𝑢 = 𝑡 )
53 opeq1 ⊢ ( 𝑢 = 𝑡 → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑡 , 𝑣 ⟩ )
54 53 eqeq2d ⊢ ( 𝑢 = 𝑡 → ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ↔ 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ ) )
55 54 biimpac ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 = 𝑡 ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
56 52 55 sylan2b ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 ∈ { 𝑡 } ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
57 56 adantrr ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
58 57 exlimiv ⊢ ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) → 𝑥 = ⟨ 𝑡 , 𝑣 ⟩ )
59 velsn ⊢ ( 𝑢 ∈ { 𝑔 } ↔ 𝑢 = 𝑔 )
60 opeq1 ⊢ ( 𝑢 = 𝑔 → ⟨ 𝑢 , 𝑦 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ )
61 60 eqeq2d ⊢ ( 𝑢 = 𝑔 → ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ↔ 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ ) )
62 61 biimpac ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ 𝑢 = 𝑔 ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
63 59 62 sylan2b ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ 𝑢 ∈ { 𝑔 } ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
64 63 adantrr ⊢ ( ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
65 64 exlimiv ⊢ ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) → 𝑥 = ⟨ 𝑔 , 𝑦 ⟩ )
66 58 65 sylan9req ⊢ ( ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → ⟨ 𝑡 , 𝑣 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ )
67 vex ⊢ 𝑡 ∈ V
68 vex ⊢ 𝑣 ∈ V
69 67 68 opth1 ⊢ ( ⟨ 𝑡 , 𝑣 ⟩ = ⟨ 𝑔 , 𝑦 ⟩ → 𝑡 = 𝑔 )
70 66 69 syl ⊢ ( ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → 𝑡 = 𝑔 )
71 70 exlimivv ⊢ ( ∃ 𝑣 ∃ 𝑦 ( ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ { 𝑡 } ∧ 𝑣 ∈ 𝑡 ) ) ∧ ∃ 𝑢 ( 𝑥 = ⟨ 𝑢 , 𝑦 ⟩ ∧ ( 𝑢 ∈ { 𝑔 } ∧ 𝑦 ∈ 𝑔 ) ) ) → 𝑡 = 𝑔 )
72 51 71 syl6 ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑡 = 𝑔 ) )
73 72 25 syl6 ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) ) )
74 eqeq12 ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( 𝑧 = 𝑤 ↔ ( { 𝑡 } × 𝑡 ) = ( { 𝑔 } × 𝑔 ) ) )
75 73 74 sylibrd ⊢ ( ( 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
76 75 ex ⊢ ( 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
77 76 rexlimivw ⊢ ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) → ( 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
78 77 rexlimdvw ⊢ ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) → ( ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) ) )
79 78 imp ⊢ ( ( ∃ 𝑡 ∈ ℎ 𝑧 = ( { 𝑡 } × 𝑡 ) ∧ ∃ 𝑔 ∈ ℎ 𝑤 = ( { 𝑔 } × 𝑔 ) ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
80 14 28 79 syl2an ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
81 12 80 biimtrrid ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) → 𝑧 = 𝑤 ) )
82 81 necon1ad ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) ) )
83 82 alrimdv ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) ) )
84 disj1 ⊢ ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤 ) )
85 83 84 imbitrrdi ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
86 85 rgen2 ⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )
87 vex ⊢ ℎ ∈ V
88 vuniex ⊢ ∪ ℎ ∈ V
89 87 88 xpex ⊢ ( ℎ × ∪ ℎ ) ∈ V
90 89 pwex ⊢ 𝒫 ( ℎ × ∪ ℎ ) ∈ V
91 snssi ⊢ ( 𝑡 ∈ ℎ → { 𝑡 } ⊆ ℎ )
92 elssuni ⊢ ( 𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ )
93 xpss12 ⊢ ( ( { 𝑡 } ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ ) → ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
94 91 92 93 syl2anc ⊢ ( 𝑡 ∈ ℎ → ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
95 vsnex ⊢ { 𝑡 } ∈ V
96 95 67 xpex ⊢ ( { 𝑡 } × 𝑡 ) ∈ V
97 96 elpw ⊢ ( ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) ↔ ( { 𝑡 } × 𝑡 ) ⊆ ( ℎ × ∪ ℎ ) )
98 94 97 sylibr ⊢ ( 𝑡 ∈ ℎ → ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) )
99 eleq1 ⊢ ( 𝑢 = ( { 𝑡 } × 𝑡 ) → ( 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) ↔ ( { 𝑡 } × 𝑡 ) ∈ 𝒫 ( ℎ × ∪ ℎ ) ) )
100 98 99 syl5ibrcom ⊢ ( 𝑡 ∈ ℎ → ( 𝑢 = ( { 𝑡 } × 𝑡 ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) ) )
101 100 rexlimiv ⊢ ( ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) )
102 101 adantl ⊢ ( ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) → 𝑢 ∈ 𝒫 ( ℎ × ∪ ℎ ) )
103 102 abssi ⊢ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ⊆ 𝒫 ( ℎ × ∪ ℎ )
104 90 103 ssexi ⊢ { 𝑢 ∣ ( 𝑢 ≠ ∅ ∧ ∃ 𝑡 ∈ ℎ 𝑢 = ( { 𝑡 } × 𝑡 ) ) } ∈ V
105 1 104 eqeltri ⊢ 𝐴 ∈ V
106 raleq ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ) )
107 raleq ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
108 107 raleqbi1dv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
109 106 108 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ↔ ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) )
110 raleq ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
111 110 exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
112 109 111 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
113 105 112 spcv ⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
114 2 113 sylbi ⊢ ( 𝜑 → ( ( ∀ 𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
115 11 86 114 mp2ani ⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )