Metamath Proof Explorer

Theorem ttcmin

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

Ref Expression
Assertion ttcmin ( ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 ) → TC+ 𝐴 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-ttc ⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
2 ssel2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
3 rdgfun ⊢ Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } )
4 funiunfv ⊢ ( Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) → ∪ 𝑧 ∈ ω ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
5 3 4 ax-mp ⊢ ∪ 𝑧 ∈ ω ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
6 fveq2 ⊢ ( 𝑧 = ∅ → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ ∅ ) )
7 6 sseq1d ⊢ ( 𝑧 = ∅ → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 ↔ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ ∅ ) ⊆ 𝐵 ) )
8 fveq2 ⊢ ( 𝑧 = 𝑤 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
9 8 sseq1d ⊢ ( 𝑧 = 𝑤 → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 ↔ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) )
10 fveq2 ⊢ ( 𝑧 = suc 𝑤 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) )
11 10 sseq1d ⊢ ( 𝑧 = suc 𝑤 → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 ↔ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) ⊆ 𝐵 ) )
12 vsnex ⊢ { 𝑥 } ∈ V
13 12 rdg0 ⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ ∅ ) = { 𝑥 }
14 snssi ⊢ ( 𝑥 ∈ 𝐵 → { 𝑥 } ⊆ 𝐵 )
15 13 14 eqsstrid ⊢ ( 𝑥 ∈ 𝐵 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ ∅ ) ⊆ 𝐵 )
16 15 adantr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ ∅ ) ⊆ 𝐵 )
17 nnon ⊢ ( 𝑤 ∈ ω → 𝑤 ∈ On )
18 fvex ⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ∈ V
19 18 uniex ⊢ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ∈ V
20 eqid ⊢ rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) = rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } )
21 unieq ⊢ ( 𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦 )
22 unieq ⊢ ( 𝑧 = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) → ∪ 𝑧 = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
23 20 21 22 rdgsucmpt2 ⊢ ( ( 𝑤 ∈ On ∧ ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ∈ V ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
24 17 19 23 sylancl ⊢ ( 𝑤 ∈ ω → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
25 24 3ad2ant1 ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) = ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) )
26 uniss ⊢ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ ∪ 𝐵 )
27 26 3ad2ant3 ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ ∪ 𝐵 )
28 simp2r ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → Tr 𝐵 )
29 df-tr ⊢ ( Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵 )
30 28 29 sylib ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → ∪ 𝐵 ⊆ 𝐵 )
31 27 30 sstrd ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 )
32 25 31 eqsstrd ⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) ⊆ 𝐵 )
33 32 3exp ⊢ ( 𝑤 ∈ ω → ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑤 ) ⊆ 𝐵 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ suc 𝑤 ) ⊆ 𝐵 ) ) )
34 7 9 11 16 33 finds2 ⊢ ( 𝑧 ∈ ω → ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 ) )
35 34 impcom ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) ∧ 𝑧 ∈ ω ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 )
36 35 iunssd ⊢ ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) → ∪ 𝑧 ∈ ω ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) ‘ 𝑧 ) ⊆ 𝐵 )
37 5 36 eqsstrrid ⊢ ( ( 𝑥 ∈ 𝐵 ∧ Tr 𝐵 ) → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ⊆ 𝐵 )
38 2 37 sylan ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ Tr 𝐵 ) → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ⊆ 𝐵 )
39 38 an32s ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ⊆ 𝐵 )
40 39 iunssd ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) ⊆ 𝐵 )
41 1 40 eqsstrid ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ Tr 𝐵 ) → TC+ 𝐴 ⊆ 𝐵 )