Metamath Proof Explorer


Theorem tskr1om2

Description: A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by NM, 22-Feb-2011)

Ref Expression
Assertion tskr1om2 T Tarski T R1 ω T

Proof

Step Hyp Ref Expression
1 eluni2 y R1 ω x R1 ω y x
2 r1fnon R1 Fn On
3 fnfun R1 Fn On Fun R1
4 2 3 ax-mp Fun R1
5 fvelima Fun R1 x R1 ω y ω R1 y = x
6 4 5 mpan x R1 ω y ω R1 y = x
7 r1tr Tr R1 y
8 treq R1 y = x Tr R1 y Tr x
9 7 8 mpbii R1 y = x Tr x
10 9 rexlimivw y ω R1 y = x Tr x
11 trss Tr x y x y x
12 6 10 11 3syl x R1 ω y x y x
13 12 adantl T Tarski T x R1 ω y x y x
14 tskr1om T Tarski T R1 ω T
15 14 sseld T Tarski T x R1 ω x T
16 tskss T Tarski x T y x y T
17 16 3exp T Tarski x T y x y T
18 17 adantr T Tarski T x T y x y T
19 15 18 syld T Tarski T x R1 ω y x y T
20 19 imp T Tarski T x R1 ω y x y T
21 13 20 syld T Tarski T x R1 ω y x y T
22 21 rexlimdva T Tarski T x R1 ω y x y T
23 1 22 syl5bi T Tarski T y R1 ω y T
24 23 ssrdv T Tarski T R1 ω T