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 e. Tarski /\ A e. On /\ A ~< T ) -> A e. T )

Proof

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