Metamath Proof Explorer

Theorem dfttc4lem2

Description: Lemma for dfttc4 . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Hypothesis dfttc4lem2.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
Assertion dfttc4lem2 ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 )

Proof

Step Hyp Ref Expression
1 dfttc4lem2.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
2 disjsn ⊢ ( ( 𝐴 ∩ { 𝑢 } ) = ∅ ↔ ¬ 𝑢 ∈ 𝐴 )
3 2 biimpi ⊢ ( ( 𝐴 ∩ { 𝑢 } ) = ∅ → ¬ 𝑢 ∈ 𝐴 )
4 3 necon2ai ⊢ ( 𝑢 ∈ 𝐴 → ( 𝐴 ∩ { 𝑢 } ) ≠ ∅ )
5 elsni ⊢ ( 𝑧 ∈ { 𝑢 } → 𝑧 = 𝑢 )
6 5 a1d ⊢ ( 𝑧 ∈ { 𝑢 } → ( ( 𝑧 ∩ { 𝑢 } ) = ∅ → 𝑧 = 𝑢 ) )
7 6 rgen ⊢ ∀ 𝑧 ∈ { 𝑢 } ( ( 𝑧 ∩ { 𝑢 } ) = ∅ → 𝑧 = 𝑢 )
8 vsnex ⊢ { 𝑢 } ∈ V
9 vex ⊢ 𝑢 ∈ V
10 1 8 9 dfttc4lem1 ⊢ ( ( ( 𝐴 ∩ { 𝑢 } ) ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 } ( ( 𝑧 ∩ { 𝑢 } ) = ∅ → 𝑧 = 𝑢 ) ) → 𝑢 ∈ 𝐵 )
11 4 7 10 sylancl ⊢ ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵 )
12 11 ssriv ⊢ 𝐴 ⊆ 𝐵
13 vex ⊢ 𝑣 ∈ V
14 simpr ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
15 14 ineq2d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑤 ) )
16 15 neeq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ↔ ( 𝐴 ∩ 𝑤 ) ≠ ∅ ) )
17 14 ineq2d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑤 ) )
18 17 eqeq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( 𝑧 ∩ 𝑦 ) = ∅ ↔ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
19 simpl ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑣 )
20 19 eqeq2d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑣 ) )
21 18 20 imbi12d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) )
22 14 21 raleqbidvv ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) )
23 16 22 anbi12d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) ) )
24 23 cbvexdvaw ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ∃ 𝑤 ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) ) )
25 13 24 1 elab2 ⊢ ( 𝑣 ∈ 𝐵 ↔ ∃ 𝑤 ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) )
26 undisj2 ⊢ ( ( ( 𝐴 ∩ 𝑤 ) = ∅ ∧ ( 𝐴 ∩ { 𝑢 } ) = ∅ ) ↔ ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ )
27 26 biimpri ⊢ ( ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( ( 𝐴 ∩ 𝑤 ) = ∅ ∧ ( 𝐴 ∩ { 𝑢 } ) = ∅ ) )
28 27 simpld ⊢ ( ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( 𝐴 ∩ 𝑤 ) = ∅ )
29 28 necon3i ⊢ ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ → ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) ≠ ∅ )
30 29 a1i ⊢ ( 𝑢 ∈ 𝑣 → ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ → ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) ≠ ∅ ) )
31 undisj2 ⊢ ( ( ( 𝑧 ∩ 𝑤 ) = ∅ ∧ ( 𝑧 ∩ { 𝑢 } ) = ∅ ) ↔ ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ )
32 31 biimpri ⊢ ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( ( 𝑧 ∩ 𝑤 ) = ∅ ∧ ( 𝑧 ∩ { 𝑢 } ) = ∅ ) )
33 32 simpld ⊢ ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( 𝑧 ∩ 𝑤 ) = ∅ )
34 33 imim1i ⊢ ( ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) → ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑣 ) )
35 32 simprd ⊢ ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( 𝑧 ∩ { 𝑢 } ) = ∅ )
36 disjsn ⊢ ( ( 𝑧 ∩ { 𝑢 } ) = ∅ ↔ ¬ 𝑢 ∈ 𝑧 )
37 35 36 sylib ⊢ ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ¬ 𝑢 ∈ 𝑧 )
38 elequ2 ⊢ ( 𝑧 = 𝑣 → ( 𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑣 ) )
39 38 biimprd ⊢ ( 𝑧 = 𝑣 → ( 𝑢 ∈ 𝑣 → 𝑢 ∈ 𝑧 ) )
40 39 con3d ⊢ ( 𝑧 = 𝑣 → ( ¬ 𝑢 ∈ 𝑧 → ¬ 𝑢 ∈ 𝑣 ) )
41 pm2.21 ⊢ ( ¬ 𝑢 ∈ 𝑣 → ( 𝑢 ∈ 𝑣 → 𝑧 = 𝑢 ) )
42 37 40 41 syl56 ⊢ ( 𝑧 = 𝑣 → ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( 𝑢 ∈ 𝑣 → 𝑧 = 𝑢 ) ) )
43 34 42 syli ⊢ ( ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) → ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → ( 𝑢 ∈ 𝑣 → 𝑧 = 𝑢 ) ) )
44 43 com3r ⊢ ( 𝑢 ∈ 𝑣 → ( ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) → ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) )
45 44 ralimdv ⊢ ( 𝑢 ∈ 𝑣 → ( ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) → ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) )
46 5 a1d ⊢ ( 𝑧 ∈ { 𝑢 } → ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) )
47 46 rgen ⊢ ∀ 𝑧 ∈ { 𝑢 } ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 )
48 ralun ⊢ ( ( ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ∧ ∀ 𝑧 ∈ { 𝑢 } ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) → ∀ 𝑧 ∈ ( 𝑤 ∪ { 𝑢 } ) ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) )
49 47 48 mpan2 ⊢ ( ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) → ∀ 𝑧 ∈ ( 𝑤 ∪ { 𝑢 } ) ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) )
50 45 49 syl6 ⊢ ( 𝑢 ∈ 𝑣 → ( ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) → ∀ 𝑧 ∈ ( 𝑤 ∪ { 𝑢 } ) ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) )
51 30 50 anim12d ⊢ ( 𝑢 ∈ 𝑣 → ( ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) → ( ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) ≠ ∅ ∧ ∀ 𝑧 ∈ ( 𝑤 ∪ { 𝑢 } ) ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) ) )
52 vex ⊢ 𝑤 ∈ V
53 52 8 unex ⊢ ( 𝑤 ∪ { 𝑢 } ) ∈ V
54 1 53 9 dfttc4lem1 ⊢ ( ( ( 𝐴 ∩ ( 𝑤 ∪ { 𝑢 } ) ) ≠ ∅ ∧ ∀ 𝑧 ∈ ( 𝑤 ∪ { 𝑢 } ) ( ( 𝑧 ∩ ( 𝑤 ∪ { 𝑢 } ) ) = ∅ → 𝑧 = 𝑢 ) ) → 𝑢 ∈ 𝐵 )
55 51 54 syl6 ⊢ ( 𝑢 ∈ 𝑣 → ( ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) → 𝑢 ∈ 𝐵 ) )
56 55 exlimdv ⊢ ( 𝑢 ∈ 𝑣 → ( ∃ 𝑤 ( ( 𝐴 ∩ 𝑤 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑤 ( ( 𝑧 ∩ 𝑤 ) = ∅ → 𝑧 = 𝑣 ) ) → 𝑢 ∈ 𝐵 ) )
57 25 56 biimtrid ⊢ ( 𝑢 ∈ 𝑣 → ( 𝑣 ∈ 𝐵 → 𝑢 ∈ 𝐵 ) )
58 57 imp ⊢ ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
59 58 gen2 ⊢ ∀ 𝑢 ∀ 𝑣 ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
60 dftr2 ⊢ ( Tr 𝐵 ↔ ∀ 𝑢 ∀ 𝑣 ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 ) )
61 59 60 mpbir ⊢ Tr 𝐵
62 12 61 pm3.2i ⊢ ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 )