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

Metamath Proof Explorer

Theorem dfac5lem4OLD

Description: Obsolete version of dfac5lem4 as of 23-Jun-2025. (Contributed by NM, 11-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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