Metamath Proof Explorer

Theorem ttctr

Description: The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttctr Tr TC+ 𝐴

Proof

Step Hyp Ref Expression
1 rdgfun ⊢ Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } )
2 eluniima ⊢ ( Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) → ( 𝑣 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑧 ∈ ω 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) )
3 1 2 ax-mp ⊢ ( 𝑣 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑧 ∈ ω 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) )
4 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
5 elunii ⊢ ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) → 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) )
6 nnon ⊢ ( 𝑧 ∈ ω → 𝑧 ∈ On )
7 fvex ⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ∈ V
8 7 uniex ⊢ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ∈ V
9 eqid ⊢ rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) = rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } )
10 unieq ⊢ ( 𝑤 = 𝑦 → ∪ 𝑤 = ∪ 𝑦 )
11 unieq ⊢ ( 𝑤 = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) → ∪ 𝑤 = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) )
12 9 10 11 rdgsucmpt2 ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ∈ V ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) )
13 6 8 12 sylancl ⊢ ( 𝑧 ∈ ω → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) )
14 13 eleq2d ⊢ ( 𝑧 ∈ ω → ( 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) ↔ 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) )
15 14 biimpar ⊢ ( ( 𝑧 ∈ ω ∧ 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) → 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) )
16 5 15 sylan2 ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) ) → 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) )
17 fveq2 ⊢ ( 𝑤 = suc 𝑧 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) )
18 17 eleq2d ⊢ ( 𝑤 = suc 𝑧 → ( 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ↔ 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) ) )
19 18 rspcev ⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑧 ) ) → ∃ 𝑤 ∈ ω 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
20 4 16 19 syl2an2r ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) ) → ∃ 𝑤 ∈ ω 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
21 eluniima ⊢ ( Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) → ( 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑤 ∈ ω 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ) )
22 1 21 ax-mp ⊢ ( 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑤 ∈ ω 𝑢 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
23 20 22 sylibr ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) ) → 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
24 23 an12s ⊢ ( ( 𝑢 ∈ 𝑣 ∧ ( 𝑧 ∈ ω ∧ 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ) ) → 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
25 24 rexlimdvaa ⊢ ( 𝑢 ∈ 𝑣 → ( ∃ 𝑧 ∈ ω 𝑣 ∈ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) → 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ) )
26 3 25 biimtrid ⊢ ( 𝑢 ∈ 𝑣 → ( 𝑣 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) → 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ) )
27 26 reximdv ⊢ ( 𝑢 ∈ 𝑣 → ( ∃ 𝑥 ∈ 𝐴 𝑣 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) → ∃ 𝑥 ∈ 𝐴 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ) )
28 eliun ⊢ ( 𝑣 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑥 ∈ 𝐴 𝑣 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
29 eliun ⊢ ( 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
30 27 28 29 3imtr4g ⊢ ( 𝑢 ∈ 𝑣 → ( 𝑣 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) → 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ) )
31 df-ttc ⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
32 31 eleq2i ⊢ ( 𝑣 ∈ TC+ 𝐴 ↔ 𝑣 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
33 31 eleq2i ⊢ ( 𝑢 ∈ TC+ 𝐴 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
34 30 32 33 3imtr4g ⊢ ( 𝑢 ∈ 𝑣 → ( 𝑣 ∈ TC+ 𝐴 → 𝑢 ∈ TC+ 𝐴 ) )
35 34 imp ⊢ ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ TC+ 𝐴 ) → 𝑢 ∈ TC+ 𝐴 )
36 35 gen2 ⊢ ∀ 𝑢 ∀ 𝑣 ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ TC+ 𝐴 ) → 𝑢 ∈ TC+ 𝐴 )
37 dftr2 ⊢ ( Tr TC+ 𝐴 ↔ ∀ 𝑢 ∀ 𝑣 ( ( 𝑢 ∈ 𝑣 ∧ 𝑣 ∈ TC+ 𝐴 ) → 𝑢 ∈ TC+ 𝐴 ) )
38 36 37 mpbir ⊢ Tr TC+ 𝐴