Metamath Proof Explorer


Theorem tskord

Description: A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion tskord T Tarski A On A T A T

Proof

Step Hyp Ref Expression
1 breq1 x = y x T y T
2 1 anbi2d x = y T Tarski x T T Tarski y T
3 eleq1 x = y x T y T
4 2 3 imbi12d x = y T Tarski x T x T T Tarski y T y T
5 breq1 x = A x T A T
6 5 anbi2d x = A T Tarski x T T Tarski A T
7 eleq1 x = A x T A T
8 6 7 imbi12d x = A T Tarski x T x T T Tarski A T A T
9 simplrl x On T Tarski x T y x T Tarski
10 onelss x On y x y x
11 ssdomg x On y x y x
12 10 11 syld x On y x y x
13 12 imp x On y x y x
14 13 adantlr x On T Tarski x T y x y x
15 simplrr x On T Tarski x T y x x T
16 domsdomtr y x x T y T
17 14 15 16 syl2anc x On T Tarski x T y x y T
18 pm2.27 T Tarski y T T Tarski y T y T y T
19 9 17 18 syl2anc x On T Tarski x T y x T Tarski y T y T y T
20 19 ralimdva x On T Tarski x T y x T Tarski y T y T y x y T
21 dfss3 x T y x y T
22 tskssel T Tarski x T x T x T
23 22 3exp T Tarski x T x T x T
24 21 23 syl5bir T Tarski y x y T x T x T
25 24 com23 T Tarski x T y x y T x T
26 25 imp T Tarski x T y x y T x T
27 26 adantl x On T Tarski x T y x y T x T
28 20 27 syld x On T Tarski x T y x T Tarski y T y T x T
29 28 ex x On T Tarski x T y x T Tarski y T y T x T
30 29 com23 x On y x T Tarski y T y T T Tarski x T x T
31 4 8 30 tfis3 A On T Tarski A T A T
32 31 3impib A On T Tarski A T A T
33 32 3com12 T Tarski A On A T A T