Metamath Proof Explorer

Theorem dfttc4

Description: An alternative expression for the transitive closure of a class, assuming Regularity. A set x is contained in the transitive closure of A iff we can construct an e. -chain from x to an element of A . This weak definition is primarily useful for proving elttcirr . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc4 TC+ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
2 1 dfttc4lem2 ⊢ ( 𝐴 ⊆ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } ∧ Tr { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } )
3 ttcmin ⊢ ( ( 𝐴 ⊆ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } ∧ Tr { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } ) → TC+ 𝐴 ⊆ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } )
4 2 3 ax-mp ⊢ TC+ 𝐴 ⊆ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }
5 vex ⊢ 𝑤 ∈ V
6 equequ2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑤 ) )
7 6 imbi2d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) )
9 8 anbi2d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) ) )
10 9 exbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) ) )
11 5 10 elab ⊢ ( 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } ↔ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) )
12 vex ⊢ 𝑦 ∈ V
13 12 inex2 ⊢ ( TC+ 𝐴 ∩ 𝑦 ) ∈ V
14 ttcid ⊢ 𝐴 ⊆ TC+ 𝐴
15 ssrin ⊢ ( 𝐴 ⊆ TC+ 𝐴 → ( 𝐴 ∩ 𝑦 ) ⊆ ( TC+ 𝐴 ∩ 𝑦 ) )
16 14 15 ax-mp ⊢ ( 𝐴 ∩ 𝑦 ) ⊆ ( TC+ 𝐴 ∩ 𝑦 )
17 ssn0 ⊢ ( ( ( 𝐴 ∩ 𝑦 ) ⊆ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝐴 ∩ 𝑦 ) ≠ ∅ ) → ( TC+ 𝐴 ∩ 𝑦 ) ≠ ∅ )
18 16 17 mpan ⊢ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ → ( TC+ 𝐴 ∩ 𝑦 ) ≠ ∅ )
19 zfreg ⊢ ( ( ( TC+ 𝐴 ∩ 𝑦 ) ∈ V ∧ ( TC+ 𝐴 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ )
20 13 18 19 sylancr ⊢ ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ → ∃ 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ )
21 simpl ⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) )
22 21 elin2d ⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → 𝑥 ∈ 𝑦 )
23 inass ⊢ ( ( 𝑥 ∩ TC+ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) )
24 elinel1 ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → 𝑥 ∈ TC+ 𝐴 )
25 ttctr2 ⊢ ( 𝑥 ∈ TC+ 𝐴 → 𝑥 ⊆ TC+ 𝐴 )
26 24 25 syl ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → 𝑥 ⊆ TC+ 𝐴 )
27 dfss2 ⊢ ( 𝑥 ⊆ TC+ 𝐴 ↔ ( 𝑥 ∩ TC+ 𝐴 ) = 𝑥 )
28 26 27 sylib ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → ( 𝑥 ∩ TC+ 𝐴 ) = 𝑥 )
29 28 ineq1d ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → ( ( 𝑥 ∩ TC+ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∩ 𝑦 ) )
30 23 29 eqtr3id ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ( 𝑥 ∩ 𝑦 ) )
31 30 eqeq1d ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → ( ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
32 31 biimpa ⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
33 ineq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∩ 𝑦 ) = ( 𝑥 ∩ 𝑦 ) )
34 33 eqeq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∩ 𝑦 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
35 equequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝑤 ↔ 𝑥 = 𝑤 ) )
36 34 35 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ↔ ( ( 𝑥 ∩ 𝑦 ) = ∅ → 𝑥 = 𝑤 ) ) )
37 36 rspcv ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → 𝑥 = 𝑤 ) ) )
38 37 com23 ⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → 𝑥 = 𝑤 ) ) )
39 22 32 38 sylc ⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → 𝑥 = 𝑤 ) )
40 39 com12 ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → 𝑥 = 𝑤 ) )
41 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ↔ 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ) )
42 41 biimpcd ⊢ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) → ( 𝑥 = 𝑤 → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ) )
43 42 adantr ⊢ ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → ( 𝑥 = 𝑤 → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ) )
44 40 43 sylcom ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → ( ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ) )
45 44 imp ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ∧ ( 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ∧ ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ ) ) → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) )
46 45 rexlimdvaa ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) → ( ∃ 𝑥 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ( 𝑥 ∩ ( TC+ 𝐴 ∩ 𝑦 ) ) = ∅ → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) ) )
47 20 46 mpan9 ⊢ ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) → 𝑤 ∈ ( TC+ 𝐴 ∩ 𝑦 ) )
48 47 elin1d ⊢ ( ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) → 𝑤 ∈ TC+ 𝐴 )
49 48 exlimiv ⊢ ( ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑤 ) ) → 𝑤 ∈ TC+ 𝐴 )
50 11 49 sylbi ⊢ ( 𝑤 ∈ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } → 𝑤 ∈ TC+ 𝐴 )
51 50 ssriv ⊢ { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) } ⊆ TC+ 𝐴
52 4 51 eqssi ⊢ TC+ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ( ( 𝐴 ∩ 𝑦 ) ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 ∩ 𝑦 ) = ∅ → 𝑧 = 𝑥 ) ) }