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 \in V \land \{x \in 𝒫 A \| x ≺ A\} \subseteq A) \to A \in dom card$

Proof

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

Metamath Proof Explorer

Theorem tskwe

Proof