r0weon

Description: A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of TakeutiZaring p. 54. (Contributed by Mario Carneiro, 7-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	leweon.1	$⊢ L = \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\}$
	r0weon.1	$⊢ R = \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w)))\}$
Assertion	r0weon	$⊢ (R We (On \times On) \land R Se (On \times On))$

Proof

Step	Hyp	Ref	Expression
1		leweon.1	$⊢ L = \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\}$
2		r0weon.1	$⊢ R = \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w)))\}$
3		fveq2	$⊢ x = z \to 1^{st} (x) = 1^{st} (z)$
4		fveq2	$⊢ x = z \to 2^{nd} (x) = 2^{nd} (z)$
5	3 4	uneq12d	$⊢ x = z \to 1^{st} (x) \cup 2^{nd} (x) = 1^{st} (z) \cup 2^{nd} (z)$
6		eqid	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
7		fvex	$⊢ 1^{st} (z) \in V$
8		fvex	$⊢ 2^{nd} (z) \in V$
9	7 8	unex	$⊢ 1^{st} (z) \cup 2^{nd} (z) \in V$
10	5 6 9	fvmpt	$⊢ z \in (On \times On) \to (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = 1^{st} (z) \cup 2^{nd} (z)$
11		fveq2	$⊢ x = w \to 1^{st} (x) = 1^{st} (w)$
12		fveq2	$⊢ x = w \to 2^{nd} (x) = 2^{nd} (w)$
13	11 12	uneq12d	$⊢ x = w \to 1^{st} (x) \cup 2^{nd} (x) = 1^{st} (w) \cup 2^{nd} (w)$
14		fvex	$⊢ 1^{st} (w) \in V$
15		fvex	$⊢ 2^{nd} (w) \in V$
16	14 15	unex	$⊢ 1^{st} (w) \cup 2^{nd} (w) \in V$
17	13 6 16	fvmpt	$⊢ w \in (On \times On) \to (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) = 1^{st} (w) \cup 2^{nd} (w)$
18	10 17	breqan12d	$⊢ (z \in (On \times On) \land w \in (On \times On)) \to ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \leftrightarrow (1^{st} (z) \cup 2^{nd} (z)) E (1^{st} (w) \cup 2^{nd} (w)))$
19	16	epeli	$⊢ (1^{st} (z) \cup 2^{nd} (z)) E (1^{st} (w) \cup 2^{nd} (w)) \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w))$
20	18 19	bitrdi	$⊢ (z \in (On \times On) \land w \in (On \times On)) \to ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)))$
21	10 17	eqeqan12d	$⊢ (z \in (On \times On) \land w \in (On \times On)) \to ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w))$
22	21	anbi1d	$⊢ (z \in (On \times On) \land w \in (On \times On)) \to (((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \land z L w) \leftrightarrow (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w))$
23	20 22	orbi12d	$⊢ (z \in (On \times On) \land w \in (On \times On)) \to (((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \lor ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \land z L w)) \leftrightarrow (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w)))$
24	23	pm5.32i	$⊢ ((z \in (On \times On) \land w \in (On \times On)) \land ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \lor ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \land z L w))) \leftrightarrow ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w)))$
25	24	opabbii	$⊢ \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \lor ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \land z L w)))\} = \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w)))\}$
26	2 25	eqtr4i	$⊢ R = \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) E (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \lor ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (z) = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) (w) \land z L w)))\}$
27		xp1st	$⊢ x \in (On \times On) \to 1^{st} (x) \in On$
28		xp2nd	$⊢ x \in (On \times On) \to 2^{nd} (x) \in On$
29		fvex	$⊢ 1^{st} (x) \in V$
30	29	elon	$⊢ 1^{st} (x) \in On \leftrightarrow Ord 1^{st} (x)$
31		fvex	$⊢ 2^{nd} (x) \in V$
32	31	elon	$⊢ 2^{nd} (x) \in On \leftrightarrow Ord 2^{nd} (x)$
33		ordun	$⊢ (Ord 1^{st} (x) \land Ord 2^{nd} (x)) \to Ord (1^{st} (x) \cup 2^{nd} (x))$
34	30 32 33	syl2anb	$⊢ (1^{st} (x) \in On \land 2^{nd} (x) \in On) \to Ord (1^{st} (x) \cup 2^{nd} (x))$
35	27 28 34	syl2anc	$⊢ x \in (On \times On) \to Ord (1^{st} (x) \cup 2^{nd} (x))$
36	29 31	unex	$⊢ 1^{st} (x) \cup 2^{nd} (x) \in V$
37	36	elon	$⊢ 1^{st} (x) \cup 2^{nd} (x) \in On \leftrightarrow Ord (1^{st} (x) \cup 2^{nd} (x))$
38	35 37	sylibr	$⊢ x \in (On \times On) \to 1^{st} (x) \cup 2^{nd} (x) \in On$
39	6 38	fmpti	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) : On \times On ⟶ On$
40	39	a1i	$⊢ ⊤ \to (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) : On \times On ⟶ On$
41		epweon	$⊢ E We On$
42	41	a1i	$⊢ ⊤ \to E We On$
43	1	leweon	$⊢ L We (On \times On)$
44	43	a1i	$⊢ ⊤ \to L We (On \times On)$
45		vex	$⊢ u \in V$
46	45	dmex	$⊢ dom u \in V$
47	45	rnex	$⊢ ran u \in V$
48	46 47	unex	$⊢ dom u \cup ran u \in V$
49		imadmres	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u})] = (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [u]$
50		inss2	$⊢ u \cap (On \times On) \subseteq On \times On$
51		ssun1	$⊢ dom u \subseteq dom u \cup ran u$
52		elinel2	$⊢ x \in (u \cap (On \times On)) \to x \in (On \times On)$
53		1st2nd2	$⊢ x \in (On \times On) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
54	52 53	syl	$⊢ x \in (u \cap (On \times On)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
55		elinel1	$⊢ x \in (u \cap (On \times On)) \to x \in u$
56	54 55	eqeltrrd	$⊢ x \in (u \cap (On \times On)) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in u$
57	29 31	opeldm	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in u \to 1^{st} (x) \in dom u$
58	56 57	syl	$⊢ x \in (u \cap (On \times On)) \to 1^{st} (x) \in dom u$
59	51 58	sseldi	$⊢ x \in (u \cap (On \times On)) \to 1^{st} (x) \in (dom u \cup ran u)$
60		ssun2	$⊢ ran u \subseteq dom u \cup ran u$
61	29 31	opelrn	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in u \to 2^{nd} (x) \in ran u$
62	56 61	syl	$⊢ x \in (u \cap (On \times On)) \to 2^{nd} (x) \in ran u$
63	60 62	sseldi	$⊢ x \in (u \cap (On \times On)) \to 2^{nd} (x) \in (dom u \cup ran u)$
64	59 63	prssd	$⊢ x \in (u \cap (On \times On)) \to \{1^{st} (x), 2^{nd} (x)\} \subseteq dom u \cup ran u$
65	52 27	syl	$⊢ x \in (u \cap (On \times On)) \to 1^{st} (x) \in On$
66	52 28	syl	$⊢ x \in (u \cap (On \times On)) \to 2^{nd} (x) \in On$
67		ordunpr	$⊢ (1^{st} (x) \in On \land 2^{nd} (x) \in On) \to 1^{st} (x) \cup 2^{nd} (x) \in \{1^{st} (x), 2^{nd} (x)\}$
68	65 66 67	syl2anc	$⊢ x \in (u \cap (On \times On)) \to 1^{st} (x) \cup 2^{nd} (x) \in \{1^{st} (x), 2^{nd} (x)\}$
69	64 68	sseldd	$⊢ x \in (u \cap (On \times On)) \to 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u)$
70	69	rgen	$⊢ \forall x \in (u \cap (On \times On)) 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u)$
71		ssrab	$⊢ u \cap (On \times On) \subseteq \{x \in (On \times On) \| 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u)\} \leftrightarrow (u \cap (On \times On) \subseteq On \times On \land \forall x \in (u \cap (On \times On)) 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u))$
72	50 70 71	mpbir2an	$⊢ u \cap (On \times On) \subseteq \{x \in (On \times On) \| 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u)\}$
73		dmres	$⊢ dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) = u \cap dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
74	39	fdmi	$⊢ dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) = On \times On$
75	74	ineq2i	$⊢ u \cap dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) = u \cap (On \times On)$
76	73 75	eqtri	$⊢ dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) = u \cap (On \times On)$
77	6	mptpreima	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [dom u \cup ran u] = \{x \in (On \times On) \| 1^{st} (x) \cup 2^{nd} (x) \in (dom u \cup ran u)\}$
78	72 76 77	3sstr4i	$⊢ dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [dom u \cup ran u]$
79		funmpt	$⊢ Fun (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
80		resss	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u} \subseteq (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
81		dmss	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u} \subseteq (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) \to dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
82	80 81	ax-mp	$⊢ dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))$
83		funimass3	$⊢ (Fun (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) \land dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq dom (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))) \to ((x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u})] \subseteq dom u \cup ran u \leftrightarrow dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [dom u \cup ran u])$
84	79 82 83	mp2an	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u})] \subseteq dom u \cup ran u \leftrightarrow dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u}) \subseteq {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [dom u \cup ran u]$
85	78 84	mpbir	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [dom ({(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) ↾}_{u})] \subseteq dom u \cup ran u$
86	49 85	eqsstrri	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [u] \subseteq dom u \cup ran u$
87	48 86	ssexi	$⊢ (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [u] \in V$
88	87	a1i	$⊢ ⊤ \to (x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x)) [u] \in V$
89	26 40 42 44 88	fnwe	$⊢ ⊤ \to R We (On \times On)$
90		epse	$⊢ E Se On$
91	90	a1i	$⊢ ⊤ \to E Se On$
92		vuniex	$⊢ ⋃ u \in V$
93	92	pwex	$⊢ 𝒫 ⋃ u \in V$
94	93 93	xpex	$⊢ 𝒫 ⋃ u \times 𝒫 ⋃ u \in V$
95	6	mptpreima	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [u] = \{x \in (On \times On) \| 1^{st} (x) \cup 2^{nd} (x) \in u\}$
96		df-rab	$⊢ \{x \in (On \times On) \| 1^{st} (x) \cup 2^{nd} (x) \in u\} = \{x \| (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u)\}$
97	95 96	eqtri	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [u] = \{x \| (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u)\}$
98	53	adantr	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
99		elssuni	$⊢ 1^{st} (x) \cup 2^{nd} (x) \in u \to 1^{st} (x) \cup 2^{nd} (x) \subseteq ⋃ u$
100	99	adantl	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to 1^{st} (x) \cup 2^{nd} (x) \subseteq ⋃ u$
101	100	unssad	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to 1^{st} (x) \subseteq ⋃ u$
102	29	elpw	$⊢ 1^{st} (x) \in 𝒫 ⋃ u \leftrightarrow 1^{st} (x) \subseteq ⋃ u$
103	101 102	sylibr	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to 1^{st} (x) \in 𝒫 ⋃ u$
104	100	unssbd	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to 2^{nd} (x) \subseteq ⋃ u$
105	31	elpw	$⊢ 2^{nd} (x) \in 𝒫 ⋃ u \leftrightarrow 2^{nd} (x) \subseteq ⋃ u$
106	104 105	sylibr	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to 2^{nd} (x) \in 𝒫 ⋃ u$
107	103 106	jca	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to (1^{st} (x) \in 𝒫 ⋃ u \land 2^{nd} (x) \in 𝒫 ⋃ u)$
108		elxp6	$⊢ x \in (𝒫 ⋃ u \times 𝒫 ⋃ u) \leftrightarrow (x = ⟨1^{st} (x), 2^{nd} (x)⟩ \land (1^{st} (x) \in 𝒫 ⋃ u \land 2^{nd} (x) \in 𝒫 ⋃ u))$
109	98 107 108	sylanbrc	$⊢ (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u) \to x \in (𝒫 ⋃ u \times 𝒫 ⋃ u)$
110	109	abssi	$⊢ \{x \| (x \in (On \times On) \land 1^{st} (x) \cup 2^{nd} (x) \in u)\} \subseteq 𝒫 ⋃ u \times 𝒫 ⋃ u$
111	97 110	eqsstri	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [u] \subseteq 𝒫 ⋃ u \times 𝒫 ⋃ u$
112	94 111	ssexi	$⊢ {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [u] \in V$
113	112	a1i	$⊢ ⊤ \to {(x \in (On \times On) ⟼ 1^{st} (x) \cup 2^{nd} (x))}^{-1} [u] \in V$
114	26 40 91 113	fnse	$⊢ ⊤ \to R Se (On \times On)$
115	89 114	jca	$⊢ ⊤ \to (R We (On \times On) \land R Se (On \times On))$
116	115	mptru	$⊢ (R We (On \times On) \land R Se (On \times On))$

Metamath Proof Explorer

Theorem r0weon

Proof