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 ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → 𝐴 ∈ dom card )

Proof

Step Hyp Ref Expression
1 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
2 rabexg ⊢ ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ∈ V )
3 incom ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ∩ On ) = ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
4 inex1g ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ∈ V → ( { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ∩ On ) ∈ V )
5 3 4 eqeltrrid ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ∈ V → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ V )
6 inss1 ⊢ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ On
7 6 sseli ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → 𝑧 ∈ On )
8 onelon ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ∈ On )
9 8 ancoms ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ On ) → 𝑦 ∈ On )
10 7 9 sylan2 ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ On )
11 onelss ⊢ ( 𝑧 ∈ On → ( 𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧 ) )
12 11 impcom ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ On ) → 𝑦 ⊆ 𝑧 )
13 7 12 sylan2 ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ⊆ 𝑧 )
14 inss2 ⊢ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 }
15 14 sseli ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
16 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴 ) )
17 16 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ≺ 𝐴 ) )
18 15 17 sylib ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → ( 𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ≺ 𝐴 ) )
19 18 simpld ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → 𝑧 ∈ 𝒫 𝐴 )
20 19 elpwid ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → 𝑧 ⊆ 𝐴 )
21 20 adantl ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑧 ⊆ 𝐴 )
22 13 21 sstrd ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ⊆ 𝐴 )
23 velpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
24 22 23 sylibr ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ 𝒫 𝐴 )
25 vex ⊢ 𝑧 ∈ V
26 ssdomg ⊢ ( 𝑧 ∈ V → ( 𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧 ) )
27 25 13 26 mpsyl ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ≼ 𝑧 )
28 18 simprd ⊢ ( 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → 𝑧 ≺ 𝐴 )
29 28 adantl ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑧 ≺ 𝐴 )
30 domsdomtr ⊢ ( ( 𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴 ) → 𝑦 ≺ 𝐴 )
31 27 29 30 syl2anc ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ≺ 𝐴 )
32 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≺ 𝐴 ↔ 𝑦 ≺ 𝐴 ) )
33 32 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ≺ 𝐴 ) )
34 24 31 33 sylanbrc ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
35 10 34 elind ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
36 35 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
37 dftr2 ⊢ ( Tr ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) → 𝑦 ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) )
38 36 37 mpbir ⊢ Tr ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
39 ordon ⊢ Ord On
40 trssord ⊢ ( ( Tr ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ On ∧ Ord On ) → Ord ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
41 38 6 39 40 mp3an ⊢ Ord ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
42 elong ⊢ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ V → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On ↔ Ord ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) )
43 41 42 mpbiri ⊢ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ V → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On )
44 1 2 5 43 4syl ⊢ ( 𝐴 ∈ 𝑉 → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On )
45 44 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On )
46 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 )
47 14 46 sstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ 𝐴 )
48 ssdomg ⊢ ( 𝐴 ∈ 𝑉 → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ 𝐴 → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≼ 𝐴 ) )
49 48 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ 𝐴 → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≼ 𝐴 ) )
50 47 49 mpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≼ 𝐴 )
51 ordirr ⊢ ( Ord ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → ¬ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
52 41 51 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ¬ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
53 44 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On )
54 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ 𝒫 𝐴 ↔ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ 𝐴 ) )
55 54 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ 𝒫 𝐴 ↔ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ⊆ 𝐴 ) )
56 47 55 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ 𝒫 𝐴 )
57 56 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ 𝒫 𝐴 )
58 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 )
59 nfcv ⊢ Ⅎ 𝑥 On
60 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 }
61 59 60 nfin ⊢ Ⅎ 𝑥 ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
62 nfcv ⊢ Ⅎ 𝑥 𝒫 𝐴
63 nfcv ⊢ Ⅎ 𝑥 ≺
64 nfcv ⊢ Ⅎ 𝑥 𝐴
65 61 63 64 nfbr ⊢ Ⅎ 𝑥 ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴
66 breq1 ⊢ ( 𝑥 = ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) → ( 𝑥 ≺ 𝐴 ↔ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) )
67 61 62 65 66 elrabf ⊢ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ↔ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ 𝒫 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) )
68 57 58 67 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } )
69 53 68 elind ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) )
70 69 3expia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ) )
71 52 70 mtod ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ¬ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 )
72 bren2 ⊢ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≈ 𝐴 ↔ ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≼ 𝐴 ∧ ¬ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≺ 𝐴 ) )
73 50 71 72 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≈ 𝐴 )
74 isnumi ⊢ ( ( ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ∈ On ∧ ( On ∩ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ) ≈ 𝐴 ) → 𝐴 ∈ dom card )
75 45 73 74 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴 } ⊆ 𝐴 ) → 𝐴 ∈ dom card )