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 
|- ( ( A C_ B /\ Tr B ) -> TC+ A C_ B )

Proof

Step Hyp Ref Expression
1 df-ttc 
 |-  TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
2 ssel2 
 |-  ( ( A C_ B /\ x e. A ) -> x e. B )
3 rdgfun 
 |-  Fun rec ( ( y e. _V |-> U. y ) , { x } )
4 funiunfv 
 |-  ( Fun rec ( ( y e. _V |-> U. y ) , { x } ) -> U_ z e. _om ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
5 3 4 ax-mp 
 |-  U_ z e. _om ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
6 fveq2 
 |-  ( z = (/) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` (/) ) )
7 6 sseq1d 
 |-  ( z = (/) -> ( ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B <-> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` (/) ) C_ B ) )
8 fveq2 
 |-  ( z = w -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
9 8 sseq1d 
 |-  ( z = w -> ( ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B <-> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) )
10 fveq2 
 |-  ( z = suc w -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) )
11 10 sseq1d 
 |-  ( z = suc w -> ( ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B <-> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) C_ B ) )
12 vsnex 
 |-  { x } e. _V
13 12 rdg0 
 |-  ( rec ( ( y e. _V |-> U. y ) , { x } ) ` (/) ) = { x }
14 snssi 
 |-  ( x e. B -> { x } C_ B )
15 13 14 eqsstrid 
 |-  ( x e. B -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` (/) ) C_ B )
16 15 adantr 
 |-  ( ( x e. B /\ Tr B ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` (/) ) C_ B )
17 nnon 
 |-  ( w e. _om -> w e. On )
18 fvex 
 |-  ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) e. _V
19 18 uniex 
 |-  U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) e. _V
20 eqid 
 |-  rec ( ( y e. _V |-> U. y ) , { x } ) = rec ( ( y e. _V |-> U. y ) , { x } )
21 unieq 
 |-  ( z = y -> U. z = U. y )
22 unieq 
 |-  ( z = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) -> U. z = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
23 20 21 22 rdgsucmpt2 
 |-  ( ( w e. On /\ U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) e. _V ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
24 17 19 23 sylancl 
 |-  ( w e. _om -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
25 24 3ad2ant1 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
26 uniss 
 |-  ( ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ U. B )
27 26 3ad2ant3 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ U. B )
28 simp2r 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> Tr B )
29 df-tr 
 |-  ( Tr B <-> U. B C_ B )
30 28 29 sylib 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> U. B C_ B )
31 27 30 sstrd 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B )
32 25 31 eqsstrd 
 |-  ( ( w e. _om /\ ( x e. B /\ Tr B ) /\ ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) C_ B )
33 32 3exp 
 |-  ( w e. _om -> ( ( x e. B /\ Tr B ) -> ( ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) C_ B -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc w ) C_ B ) ) )
34 7 9 11 16 33 finds2 
 |-  ( z e. _om -> ( ( x e. B /\ Tr B ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B ) )
35 34 impcom 
 |-  ( ( ( x e. B /\ Tr B ) /\ z e. _om ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B )
36 35 iunssd 
 |-  ( ( x e. B /\ Tr B ) -> U_ z e. _om ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) C_ B )
37 5 36 eqsstrrid 
 |-  ( ( x e. B /\ Tr B ) -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) C_ B )
38 2 37 sylan 
 |-  ( ( ( A C_ B /\ x e. A ) /\ Tr B ) -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) C_ B )
39 38 an32s 
 |-  ( ( ( A C_ B /\ Tr B ) /\ x e. A ) -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) C_ B )
40 39 iunssd 
 |-  ( ( A C_ B /\ Tr B ) -> U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) C_ B )
41 1 40 eqsstrid 
 |-  ( ( A C_ B /\ Tr B ) -> TC+ A C_ B )