canthwe

Description: The set of well-orders of a set A strictly dominates A . A stronger form of canth2 . Corollary 1.4(b) of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 31-May-2015)

		Ref	Expression
	Hypothesis	canthwe.1	$⊢ O = \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
	Assertion	canthwe	$⊢ A \in V \to A ≺ O$

Proof

Step	Hyp	Ref	Expression
1		canthwe.1	$⊢ O = \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
2		simp1	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \subseteq A$
3		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
4	2 3	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \in 𝒫 A$
5		simp2	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \subseteq x \times x$
6		xpss12	$⊢ (x \subseteq A \land x \subseteq A) \to x \times x \subseteq A \times A$
7	2 2 6	syl2anc	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \times x \subseteq A \times A$
8	5 7	sstrd	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \subseteq A \times A$
9		velpw	$⊢ r \in 𝒫 (A \times A) \leftrightarrow r \subseteq A \times A$
10	8 9	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \in 𝒫 (A \times A)$
11	4 10	jca	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to (x \in 𝒫 A \land r \in 𝒫 (A \times A))$
12	11	ssopab2i	$⊢ \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \subseteq \{⟨x, r⟩ \| (x \in 𝒫 A \land r \in 𝒫 (A \times A))\}$
13		df-xp	$⊢ 𝒫 A \times 𝒫 (A \times A) = \{⟨x, r⟩ \| (x \in 𝒫 A \land r \in 𝒫 (A \times A))\}$
14	12 1 13	3sstr4i	$⊢ O \subseteq 𝒫 A \times 𝒫 (A \times A)$
15		pwexg	$⊢ A \in V \to 𝒫 A \in V$
16		sqxpexg	$⊢ A \in V \to A \times A \in V$
17	16	pwexd	$⊢ A \in V \to 𝒫 (A \times A) \in V$
18	15 17	xpexd	$⊢ A \in V \to 𝒫 A \times 𝒫 (A \times A) \in V$
19		ssexg	$⊢ (O \subseteq 𝒫 A \times 𝒫 (A \times A) \land 𝒫 A \times 𝒫 (A \times A) \in V) \to O \in V$
20	14 18 19	sylancr	$⊢ A \in V \to O \in V$
21		simpr	$⊢ (A \in V \land u \in A) \to u \in A$
22	21	snssd	$⊢ (A \in V \land u \in A) \to \{u\} \subseteq A$
23		0ss	$⊢ \emptyset \subseteq \{u\} \times \{u\}$
24	23	a1i	$⊢ (A \in V \land u \in A) \to \emptyset \subseteq \{u\} \times \{u\}$
25		rel0	$⊢ Rel \emptyset$
26		br0	$⊢ \neg u \emptyset u$
27		wesn	$⊢ Rel \emptyset \to (\emptyset We \{u\} \leftrightarrow \neg u \emptyset u)$
28	26 27	mpbiri	$⊢ Rel \emptyset \to \emptyset We \{u\}$
29	25 28	mp1i	$⊢ (A \in V \land u \in A) \to \emptyset We \{u\}$
30		snex	$⊢ \{u\} \in V$
31		0ex	$⊢ \emptyset \in V$
32		simpl	$⊢ (x = \{u\} \land r = \emptyset) \to x = \{u\}$
33	32	sseq1d	$⊢ (x = \{u\} \land r = \emptyset) \to (x \subseteq A \leftrightarrow \{u\} \subseteq A)$
34		simpr	$⊢ (x = \{u\} \land r = \emptyset) \to r = \emptyset$
35	32	sqxpeqd	$⊢ (x = \{u\} \land r = \emptyset) \to x \times x = \{u\} \times \{u\}$
36	34 35	sseq12d	$⊢ (x = \{u\} \land r = \emptyset) \to (r \subseteq x \times x \leftrightarrow \emptyset \subseteq \{u\} \times \{u\})$
37		weeq2	$⊢ x = \{u\} \to (r We x \leftrightarrow r We \{u\})$
38		weeq1	$⊢ r = \emptyset \to (r We \{u\} \leftrightarrow \emptyset We \{u\})$
39	37 38	sylan9bb	$⊢ (x = \{u\} \land r = \emptyset) \to (r We x \leftrightarrow \emptyset We \{u\})$
40	33 36 39	3anbi123d	$⊢ (x = \{u\} \land r = \emptyset) \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (\{u\} \subseteq A \land \emptyset \subseteq \{u\} \times \{u\} \land \emptyset We \{u\}))$
41	30 31 40	opelopaba	$⊢ ⟨\{u\}, \emptyset⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\} \leftrightarrow (\{u\} \subseteq A \land \emptyset \subseteq \{u\} \times \{u\} \land \emptyset We \{u\})$
42	22 24 29 41	syl3anbrc	$⊢ (A \in V \land u \in A) \to ⟨\{u\}, \emptyset⟩ \in \{⟨x, r⟩ \| (x \subseteq A \land r \subseteq x \times x \land r We x)\}$
43	42 1	eleqtrrdi	$⊢ (A \in V \land u \in A) \to ⟨\{u\}, \emptyset⟩ \in O$
44	43	ex	$⊢ A \in V \to (u \in A \to ⟨\{u\}, \emptyset⟩ \in O)$
45		eqid	$⊢ \emptyset = \emptyset$
46		snex	$⊢ \{v\} \in V$
47	46 31	opth2	$⊢ ⟨\{u\}, \emptyset⟩ = ⟨\{v\}, \emptyset⟩ \leftrightarrow (\{u\} = \{v\} \land \emptyset = \emptyset)$
48	45 47	mpbiran2	$⊢ ⟨\{u\}, \emptyset⟩ = ⟨\{v\}, \emptyset⟩ \leftrightarrow \{u\} = \{v\}$
49		sneqbg	$⊢ u \in V \to (\{u\} = \{v\} \leftrightarrow u = v)$
50	49	elv	$⊢ \{u\} = \{v\} \leftrightarrow u = v$
51	48 50	bitri	$⊢ ⟨\{u\}, \emptyset⟩ = ⟨\{v\}, \emptyset⟩ \leftrightarrow u = v$
52	51	2a1i	$⊢ A \in V \to ((u \in A \land v \in A) \to (⟨\{u\}, \emptyset⟩ = ⟨\{v\}, \emptyset⟩ \leftrightarrow u = v))$
53	44 52	dom2d	$⊢ A \in V \to (O \in V \to A ≼ O)$
54	20 53	mpd	$⊢ A \in V \to A ≼ O$
55		eqid	$⊢ \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\}$
56	55	fpwwe2cbv	$⊢ \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / w \underset{˙}{]} w f (r \cap (w \times w)) = y))\}$
57		eqid	$⊢ ⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} = ⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\}$
58		eqid	$⊢ {\{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} (⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\})}^{-1} [\{⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} f \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} (⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\})\}] = {\{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} (⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\})}^{-1} [\{⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} f \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\} (⋃ dom \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v f (s \cap (v \times v)) = z))\})\}]$
59	1 56 57 58	canthwelem	$⊢ A \in V \to \neg f : O \underset{1-1}{⟶} A$
60		f1of1	$⊢ f : O \underset{1-1 onto}{⟶} A \to f : O \underset{1-1}{⟶} A$
61	59 60	nsyl	$⊢ A \in V \to \neg f : O \underset{1-1 onto}{⟶} A$
62	61	nexdv	$⊢ A \in V \to \neg \exists f f : O \underset{1-1 onto}{⟶} A$
63		ensym	$⊢ A \approx O \to O \approx A$
64		bren	$⊢ O \approx A \leftrightarrow \exists f f : O \underset{1-1 onto}{⟶} A$
65	63 64	sylib	$⊢ A \approx O \to \exists f f : O \underset{1-1 onto}{⟶} A$
66	62 65	nsyl	$⊢ A \in V \to \neg A \approx O$
67		brsdom	$⊢ A ≺ O \leftrightarrow (A ≼ O \land \neg A \approx O)$
68	54 66 67	sylanbrc	$⊢ A \in V \to A ≺ O$

Metamath Proof Explorer

Theorem canthwe

Proof