Metamath Proof Explorer

Theorem tskhf

Description: A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by NM, 22-Feb-2011) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

Ref Expression
Assertion tskhf 
|- ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T )

Proof

Step Hyp Ref Expression
1 df-hf 
 |-  HF = U. ( R1 " _om )
2 1 eleq2i 
 |-  ( y e. HF <-> y e. U. ( R1 " _om ) )
3 eluni2 
 |-  ( y e. U. ( R1 " _om ) <-> E. x e. ( R1 " _om ) y e. x )
4 2 3 bitri 
 |-  ( y e. HF <-> E. x e. ( R1 " _om ) y e. x )
5 r1fnon 
 |-  R1 Fn On
6 fnfun 
 |-  ( R1 Fn On -> Fun R1 )
7 5 6 ax-mp 
 |-  Fun R1
8 fvelima 
 |-  ( ( Fun R1 /\ x e. ( R1 " _om ) ) -> E. y e. _om ( R1 ` y ) = x )
9 7 8 mpan 
 |-  ( x e. ( R1 " _om ) -> E. y e. _om ( R1 ` y ) = x )
10 r1tr 
 |-  Tr ( R1 ` y )
11 treq 
 |-  ( ( R1 ` y ) = x -> ( Tr ( R1 ` y ) <-> Tr x ) )
12 10 11 mpbii 
 |-  ( ( R1 ` y ) = x -> Tr x )
13 12 rexlimivw 
 |-  ( E. y e. _om ( R1 ` y ) = x -> Tr x )
14 trss 
 |-  ( Tr x -> ( y e. x -> y C_ x ) )
15 9 13 14 3syl 
 |-  ( x e. ( R1 " _om ) -> ( y e. x -> y C_ x ) )
16 15 adantl 
 |-  ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y C_ x ) )
17 tskr1om 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )
18 17 sseld 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> x e. T ) )
19 tskss 
 |-  ( ( T e. Tarski /\ x e. T /\ y C_ x ) -> y e. T )
20 19 3exp 
 |-  ( T e. Tarski -> ( x e. T -> ( y C_ x -> y e. T ) ) )
21 20 adantr 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. T -> ( y C_ x -> y e. T ) ) )
22 18 21 syld 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> ( y C_ x -> y e. T ) ) )
23 22 imp 
 |-  ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y C_ x -> y e. T ) )
24 16 23 syld 
 |-  ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y e. T ) )
25 24 rexlimdva 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( E. x e. ( R1 " _om ) y e. x -> y e. T ) )
26 4 25 biimtrid 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. HF -> y e. T ) )
27 26 ssrdv 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T )