Metamath Proof Explorer

Theorem dfttc2g

Description: A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc2g ( 𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )

Proof

Step Hyp Ref Expression
1 rdg0g ⊢ ( 𝐴 ∈ 𝑉 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) = 𝐴 )
2 rdgfnon ⊢ rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) Fn On
3 omsson ⊢ ω ⊆ On
4 peano1 ⊢ ∅ ∈ ω
5 fnfvima ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) Fn On ∧ ω ⊆ On ∧ ∅ ∈ ω ) → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
6 2 3 4 5 mp3an ⊢ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω )
7 1 6 eqeltrrdi ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
8 elssuni ⊢ ( 𝐴 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) → 𝐴 ⊆ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
9 7 8 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
10 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
11 elunii ⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) → 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
12 nnon ⊢ ( 𝑧 ∈ ω → 𝑧 ∈ On )
13 fvex ⊢ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ∈ V
14 13 uniex ⊢ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ∈ V
15 eqid ⊢ rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) = rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 )
16 unieq ⊢ ( 𝑦 = 𝑥 → ∪ 𝑦 = ∪ 𝑥 )
17 unieq ⊢ ( 𝑦 = ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) → ∪ 𝑦 = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
18 15 16 17 rdgsucmpt2 ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ∈ V ) → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
19 12 14 18 sylancl ⊢ ( 𝑧 ∈ ω → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
20 19 eleq2d ⊢ ( 𝑧 ∈ ω → ( 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ↔ 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) )
21 20 biimpar ⊢ ( ( 𝑧 ∈ ω ∧ 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) → 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) )
22 11 21 sylan2 ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) ) → 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) )
23 fveq2 ⊢ ( 𝑦 = suc 𝑧 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) = ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) )
24 23 eleq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ↔ 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ) )
25 24 rspcev ⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ) → ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) )
26 10 22 25 syl2an2r ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) ) → ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) )
27 26 an12s ⊢ ( ( 𝑤 ∈ 𝑦 ∧ ( 𝑧 ∈ ω ∧ 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) ) → ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) )
28 27 rexlimdvaa ⊢ ( 𝑤 ∈ 𝑦 → ( ∃ 𝑧 ∈ ω 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) → ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ) )
29 rdgfun ⊢ Fun rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 )
30 eluniima ⊢ ( Fun rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) → ( 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ↔ ∃ 𝑧 ∈ ω 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ) )
31 29 30 ax-mp ⊢ ( 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ↔ ∃ 𝑧 ∈ ω 𝑦 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
32 eluniima ⊢ ( Fun rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) → ( 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ) )
33 29 32 ax-mp ⊢ ( 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑤 ∈ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) )
34 28 31 33 3imtr4g ⊢ ( 𝑤 ∈ 𝑦 → ( 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) → 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) )
35 34 imp ⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) → 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
36 35 gen2 ⊢ ∀ 𝑤 ∀ 𝑦 ( ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) → 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
37 dftr2 ⊢ ( Tr ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ↔ ∀ 𝑤 ∀ 𝑦 ( ( 𝑤 ∈ 𝑦 ∧ 𝑦 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) → 𝑤 ∈ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) )
38 36 37 mpbir ⊢ Tr ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω )
39 ttcmin ⊢ ( ( 𝐴 ⊆ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ∧ Tr ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ) → TC+ 𝐴 ⊆ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
40 9 38 39 sylancl ⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
41 funiunfv ⊢ ( Fun rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) → ∪ 𝑦 ∈ ω ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )
42 29 41 ax-mp ⊢ ∪ 𝑦 ∈ ω ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω )
43 fveq2 ⊢ ( 𝑦 = ∅ → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) = ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) )
44 43 sseq1d ⊢ ( 𝑦 = ∅ → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 ↔ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) ⊆ TC+ 𝐴 ) )
45 fveq2 ⊢ ( 𝑦 = 𝑧 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) = ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
46 45 sseq1d ⊢ ( 𝑦 = 𝑧 → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 ↔ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 ) )
47 23 sseq1d ⊢ ( 𝑦 = suc 𝑧 → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 ↔ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ⊆ TC+ 𝐴 ) )
48 ttcid ⊢ 𝐴 ⊆ TC+ 𝐴
49 1 48 eqsstrdi ⊢ ( 𝐴 ∈ 𝑉 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ ∅ ) ⊆ TC+ 𝐴 )
50 uniss ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 → ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ ∪ TC+ 𝐴 )
51 ttctr3 ⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
52 50 51 sstrdi ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 → ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 )
53 19 sseq1d ⊢ ( 𝑧 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ⊆ TC+ 𝐴 ↔ ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 ) )
54 52 53 imbitrrid ⊢ ( 𝑧 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ⊆ TC+ 𝐴 ) )
55 54 a1d ⊢ ( 𝑧 ∈ ω → ( 𝐴 ∈ 𝑉 → ( ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑧 ) ⊆ TC+ 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ suc 𝑧 ) ⊆ TC+ 𝐴 ) ) )
56 44 46 47 49 55 finds2 ⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ 𝑉 → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 ) )
57 56 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ω ) → ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 )
58 57 iunssd ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝑦 ∈ ω ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) ‘ 𝑦 ) ⊆ TC+ 𝐴 )
59 42 58 eqsstrrid ⊢ ( 𝐴 ∈ 𝑉 → ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) ⊆ TC+ 𝐴 )
60 40 59 eqssd ⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ ( rec ( ( 𝑥 ∈ V ↦ ∪ 𝑥 ) , 𝐴 ) “ ω ) )