Metamath Proof Explorer

Theorem tskwe

Description: A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion tskwe 
|- ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> A e. dom card )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | x ~< A } e. _V )
3 incom 
 |-  ( { x e. ~P A | x ~< A } i^i On ) = ( On i^i { x e. ~P A | x ~< A } )
4 inex1g 
 |-  ( { x e. ~P A | x ~< A } e. _V -> ( { x e. ~P A | x ~< A } i^i On ) e. _V )
5 3 4 eqeltrrid 
 |-  ( { x e. ~P A | x ~< A } e. _V -> ( On i^i { x e. ~P A | x ~< A } ) e. _V )
6 inss1 
 |-  ( On i^i { x e. ~P A | x ~< A } ) C_ On
7 6 sseli 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> z e. On )
8 onelon 
 |-  ( ( z e. On /\ y e. z ) -> y e. On )
9 8 ancoms 
 |-  ( ( y e. z /\ z e. On ) -> y e. On )
10 7 9 sylan2 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. On )
11 onelss 
 |-  ( z e. On -> ( y e. z -> y C_ z ) )
12 11 impcom 
 |-  ( ( y e. z /\ z e. On ) -> y C_ z )
13 7 12 sylan2 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y C_ z )
14 inss2 
 |-  ( On i^i { x e. ~P A | x ~< A } ) C_ { x e. ~P A | x ~< A }
15 14 sseli 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> z e. { x e. ~P A | x ~< A } )
16 breq1 
 |-  ( x = z -> ( x ~< A <-> z ~< A ) )
17 16 elrab 
 |-  ( z e. { x e. ~P A | x ~< A } <-> ( z e. ~P A /\ z ~< A ) )
18 15 17 sylib 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> ( z e. ~P A /\ z ~< A ) )
19 18 simpld 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> z e. ~P A )
20 19 elpwid 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> z C_ A )
21 20 adantl 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> z C_ A )
22 13 21 sstrd 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y C_ A )
23 velpw 
 |-  ( y e. ~P A <-> y C_ A )
24 22 23 sylibr 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. ~P A )
25 vex 
 |-  z e. _V
26 ssdomg 
 |-  ( z e. _V -> ( y C_ z -> y ~<_ z ) )
27 25 13 26 mpsyl 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y ~<_ z )
28 18 simprd 
 |-  ( z e. ( On i^i { x e. ~P A | x ~< A } ) -> z ~< A )
29 28 adantl 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> z ~< A )
30 domsdomtr 
 |-  ( ( y ~<_ z /\ z ~< A ) -> y ~< A )
31 27 29 30 syl2anc 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y ~< A )
32 breq1 
 |-  ( x = y -> ( x ~< A <-> y ~< A ) )
33 32 elrab 
 |-  ( y e. { x e. ~P A | x ~< A } <-> ( y e. ~P A /\ y ~< A ) )
34 24 31 33 sylanbrc 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. { x e. ~P A | x ~< A } )
35 10 34 elind 
 |-  ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. ( On i^i { x e. ~P A | x ~< A } ) )
36 35 gen2 
 |-  A. y A. z ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. ( On i^i { x e. ~P A | x ~< A } ) )
37 dftr2 
 |-  ( Tr ( On i^i { x e. ~P A | x ~< A } ) <-> A. y A. z ( ( y e. z /\ z e. ( On i^i { x e. ~P A | x ~< A } ) ) -> y e. ( On i^i { x e. ~P A | x ~< A } ) ) )
38 36 37 mpbir 
 |-  Tr ( On i^i { x e. ~P A | x ~< A } )
39 ordon 
 |-  Ord On
40 trssord 
 |-  ( ( Tr ( On i^i { x e. ~P A | x ~< A } ) /\ ( On i^i { x e. ~P A | x ~< A } ) C_ On /\ Ord On ) -> Ord ( On i^i { x e. ~P A | x ~< A } ) )
41 38 6 39 40 mp3an 
 |-  Ord ( On i^i { x e. ~P A | x ~< A } )
42 elong 
 |-  ( ( On i^i { x e. ~P A | x ~< A } ) e. _V -> ( ( On i^i { x e. ~P A | x ~< A } ) e. On <-> Ord ( On i^i { x e. ~P A | x ~< A } ) ) )
43 41 42 mpbiri 
 |-  ( ( On i^i { x e. ~P A | x ~< A } ) e. _V -> ( On i^i { x e. ~P A | x ~< A } ) e. On )
44 1 2 5 43 4syl 
 |-  ( A e. V -> ( On i^i { x e. ~P A | x ~< A } ) e. On )
45 44 adantr 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. On )
46 simpr 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> { x e. ~P A | x ~< A } C_ A )
47 14 46 sstrid 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( On i^i { x e. ~P A | x ~< A } ) C_ A )
48 ssdomg 
 |-  ( A e. V -> ( ( On i^i { x e. ~P A | x ~< A } ) C_ A -> ( On i^i { x e. ~P A | x ~< A } ) ~<_ A ) )
49 48 adantr 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( ( On i^i { x e. ~P A | x ~< A } ) C_ A -> ( On i^i { x e. ~P A | x ~< A } ) ~<_ A ) )
50 47 49 mpd 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( On i^i { x e. ~P A | x ~< A } ) ~<_ A )
51 ordirr 
 |-  ( Ord ( On i^i { x e. ~P A | x ~< A } ) -> -. ( On i^i { x e. ~P A | x ~< A } ) e. ( On i^i { x e. ~P A | x ~< A } ) )
52 41 51 mp1i 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> -. ( On i^i { x e. ~P A | x ~< A } ) e. ( On i^i { x e. ~P A | x ~< A } ) )
53 44 3ad2ant1 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. On )
54 elpw2g 
 |-  ( A e. V -> ( ( On i^i { x e. ~P A | x ~< A } ) e. ~P A <-> ( On i^i { x e. ~P A | x ~< A } ) C_ A ) )
55 54 adantr 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( ( On i^i { x e. ~P A | x ~< A } ) e. ~P A <-> ( On i^i { x e. ~P A | x ~< A } ) C_ A ) )
56 47 55 mpbird 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. ~P A )
57 56 3adant3 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. ~P A )
58 simp3 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) -> ( On i^i { x e. ~P A | x ~< A } ) ~< A )
59 nfcv 
 |-  F/_ x On
60 nfrab1 
 |-  F/_ x { x e. ~P A | x ~< A }
61 59 60 nfin 
 |-  F/_ x ( On i^i { x e. ~P A | x ~< A } )
62 nfcv 
 |-  F/_ x ~P A
63 nfcv 
 |-  F/_ x ~<
64 nfcv 
 |-  F/_ x A
65 61 63 64 nfbr 
 |-  F/ x ( On i^i { x e. ~P A | x ~< A } ) ~< A
66 breq1 
 |-  ( x = ( On i^i { x e. ~P A | x ~< A } ) -> ( x ~< A <-> ( On i^i { x e. ~P A | x ~< A } ) ~< A ) )
67 61 62 65 66 elrabf 
 |-  ( ( On i^i { x e. ~P A | x ~< A } ) e. { x e. ~P A | x ~< A } <-> ( ( On i^i { x e. ~P A | x ~< A } ) e. ~P A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) )
68 57 58 67 sylanbrc 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. { x e. ~P A | x ~< A } )
69 53 68 elind 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A /\ ( On i^i { x e. ~P A | x ~< A } ) ~< A ) -> ( On i^i { x e. ~P A | x ~< A } ) e. ( On i^i { x e. ~P A | x ~< A } ) )
70 69 3expia 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( ( On i^i { x e. ~P A | x ~< A } ) ~< A -> ( On i^i { x e. ~P A | x ~< A } ) e. ( On i^i { x e. ~P A | x ~< A } ) ) )
71 52 70 mtod 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> -. ( On i^i { x e. ~P A | x ~< A } ) ~< A )
72 bren2 
 |-  ( ( On i^i { x e. ~P A | x ~< A } ) ~~ A <-> ( ( On i^i { x e. ~P A | x ~< A } ) ~<_ A /\ -. ( On i^i { x e. ~P A | x ~< A } ) ~< A ) )
73 50 71 72 sylanbrc 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> ( On i^i { x e. ~P A | x ~< A } ) ~~ A )
74 isnumi 
 |-  ( ( ( On i^i { x e. ~P A | x ~< A } ) e. On /\ ( On i^i { x e. ~P A | x ~< A } ) ~~ A ) -> A e. dom card )
75 45 73 74 syl2anc 
 |-  ( ( A e. V /\ { x e. ~P A | x ~< A } C_ A ) -> A e. dom card )