infxpenlem

	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)))\}$
	infxpen.1	$⊢ Q = R \cap ((a \times a) \times (a \times a))$
	infxpen.2	$⊢ φ \leftrightarrow ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a))$
	infxpen.3	$⊢ M = 1^{st} (w) \cup 2^{nd} (w)$
	infxpen.4	$⊢ J = OrdIso (Q, a \times a)$
Assertion	infxpenlem	$⊢ (A \in On \land ω \subseteq A) \to (A \times A) \approx A$

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		infxpen.1	$⊢ Q = R \cap ((a \times a) \times (a \times a))$
4		infxpen.2	$⊢ φ \leftrightarrow ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a))$
5		infxpen.3	$⊢ M = 1^{st} (w) \cup 2^{nd} (w)$
6		infxpen.4	$⊢ J = OrdIso (Q, a \times a)$
7		sseq2	$⊢ a = m \to (ω \subseteq a \leftrightarrow ω \subseteq m)$
8		xpeq12	$⊢ (a = m \land a = m) \to a \times a = m \times m$
9	8	anidms	$⊢ a = m \to a \times a = m \times m$
10		id	$⊢ a = m \to a = m$
11	9 10	breq12d	$⊢ a = m \to ((a \times a) \approx a \leftrightarrow (m \times m) \approx m)$
12	7 11	imbi12d	$⊢ a = m \to ((ω \subseteq a \to (a \times a) \approx a) \leftrightarrow (ω \subseteq m \to (m \times m) \approx m))$
13		sseq2	$⊢ a = A \to (ω \subseteq a \leftrightarrow ω \subseteq A)$
14		xpeq12	$⊢ (a = A \land a = A) \to a \times a = A \times A$
15	14	anidms	$⊢ a = A \to a \times a = A \times A$
16		id	$⊢ a = A \to a = A$
17	15 16	breq12d	$⊢ a = A \to ((a \times a) \approx a \leftrightarrow (A \times A) \approx A)$
18	13 17	imbi12d	$⊢ a = A \to ((ω \subseteq a \to (a \times a) \approx a) \leftrightarrow (ω \subseteq A \to (A \times A) \approx A))$
19		vex	$⊢ a \in V$
20	19 19	xpex	$⊢ a \times a \in V$
21		simpll	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to a \in On$
22	4 21	sylbi	$⊢ φ \to a \in On$
23		onss	$⊢ a \in On \to a \subseteq On$
24	22 23	syl	$⊢ φ \to a \subseteq On$
25		xpss12	$⊢ (a \subseteq On \land a \subseteq On) \to a \times a \subseteq On \times On$
26	24 24 25	syl2anc	$⊢ φ \to a \times a \subseteq On \times On$
27	1 2	r0weon	$⊢ (R We (On \times On) \land R Se (On \times On))$
28	27	simpli	$⊢ R We (On \times On)$
29		wess	$⊢ a \times a \subseteq On \times On \to (R We (On \times On) \to R We (a \times a))$
30	26 28 29	mpisyl	$⊢ φ \to R We (a \times a)$
31		weinxp	$⊢ R We (a \times a) \leftrightarrow (R \cap ((a \times a) \times (a \times a))) We (a \times a)$
32	30 31	sylib	$⊢ φ \to (R \cap ((a \times a) \times (a \times a))) We (a \times a)$
33		weeq1	$⊢ Q = R \cap ((a \times a) \times (a \times a)) \to (Q We (a \times a) \leftrightarrow (R \cap ((a \times a) \times (a \times a))) We (a \times a))$
34	3 33	ax-mp	$⊢ Q We (a \times a) \leftrightarrow (R \cap ((a \times a) \times (a \times a))) We (a \times a)$
35	32 34	sylibr	$⊢ φ \to Q We (a \times a)$
36	6	oiiso	$⊢ (a \times a \in V \land Q We (a \times a)) \to J {Isom}_{E, Q} (dom J, a \times a)$
37	20 35 36	sylancr	$⊢ φ \to J {Isom}_{E, Q} (dom J, a \times a)$
38		isof1o	$⊢ J {Isom}_{E, Q} (dom J, a \times a) \to J : dom J \underset{1-1 onto}{⟶} a \times a$
39		f1ocnv	$⊢ J : dom J \underset{1-1 onto}{⟶} a \times a \to J^{-1} : a \times a \underset{1-1 onto}{⟶} dom J$
40		f1of1	$⊢ J^{-1} : a \times a \underset{1-1 onto}{⟶} dom J \to J^{-1} : a \times a \underset{1-1}{⟶} dom J$
41	37 38 39 40	4syl	$⊢ φ \to J^{-1} : a \times a \underset{1-1}{⟶} dom J$
42		f1f1orn	$⊢ J^{-1} : a \times a \underset{1-1}{⟶} dom J \to J^{-1} : a \times a \underset{1-1 onto}{⟶} ran J^{-1}$
43	20	f1oen	$⊢ J^{-1} : a \times a \underset{1-1 onto}{⟶} ran J^{-1} \to (a \times a) \approx ran J^{-1}$
44	41 42 43	3syl	$⊢ φ \to (a \times a) \approx ran J^{-1}$
45		f1ofn	$⊢ J^{-1} : a \times a \underset{1-1 onto}{⟶} dom J \to J^{-1} Fn (a \times a)$
46	37 38 39 45	4syl	$⊢ φ \to J^{-1} Fn (a \times a)$
47	37	adantr	$⊢ (φ \land w \in (a \times a)) \to J {Isom}_{E, Q} (dom J, a \times a)$
48	38 39 40	3syl	$⊢ J {Isom}_{E, Q} (dom J, a \times a) \to J^{-1} : a \times a \underset{1-1}{⟶} dom J$
49		cnvimass	$⊢ Q^{-1} [\{w\}] \subseteq dom Q$
50		inss2	$⊢ R \cap ((a \times a) \times (a \times a)) \subseteq (a \times a) \times (a \times a)$
51	3 50	eqsstri	$⊢ Q \subseteq (a \times a) \times (a \times a)$
52		dmss	$⊢ Q \subseteq (a \times a) \times (a \times a) \to dom Q \subseteq dom ((a \times a) \times (a \times a))$
53	51 52	ax-mp	$⊢ dom Q \subseteq dom ((a \times a) \times (a \times a))$
54		dmxpid	$⊢ dom ((a \times a) \times (a \times a)) = a \times a$
55	53 54	sseqtri	$⊢ dom Q \subseteq a \times a$
56	49 55	sstri	$⊢ Q^{-1} [\{w\}] \subseteq a \times a$
57		f1ores	$⊢ (J^{-1} : a \times a \underset{1-1}{⟶} dom J \land Q^{-1} [\{w\}] \subseteq a \times a) \to ({J^{-1} ↾}_{Q^{-1} [\{w\}]}) : Q^{-1} [\{w\}] \underset{1-1 onto}{⟶} J^{-1} [Q^{-1} [\{w\}]]$
58	48 56 57	sylancl	$⊢ J {Isom}_{E, Q} (dom J, a \times a) \to ({J^{-1} ↾}_{Q^{-1} [\{w\}]}) : Q^{-1} [\{w\}] \underset{1-1 onto}{⟶} J^{-1} [Q^{-1} [\{w\}]]$
59	20 20	xpex	$⊢ (a \times a) \times (a \times a) \in V$
60	59	inex2	$⊢ R \cap ((a \times a) \times (a \times a)) \in V$
61	3 60	eqeltri	$⊢ Q \in V$
62	61	cnvex	$⊢ Q^{-1} \in V$
63	62	imaex	$⊢ Q^{-1} [\{w\}] \in V$
64	63	f1oen	$⊢ ({J^{-1} ↾}_{Q^{-1} [\{w\}]}) : Q^{-1} [\{w\}] \underset{1-1 onto}{⟶} J^{-1} [Q^{-1} [\{w\}]] \to Q^{-1} [\{w\}] \approx J^{-1} [Q^{-1} [\{w\}]]$
65	47 58 64	3syl	$⊢ (φ \land w \in (a \times a)) \to Q^{-1} [\{w\}] \approx J^{-1} [Q^{-1} [\{w\}]]$
66		sseqin2	$⊢ Q^{-1} [\{w\}] \subseteq a \times a \leftrightarrow (a \times a) \cap Q^{-1} [\{w\}] = Q^{-1} [\{w\}]$
67	56 66	mpbi	$⊢ (a \times a) \cap Q^{-1} [\{w\}] = Q^{-1} [\{w\}]$
68	67	imaeq2i	$⊢ J^{-1} [(a \times a) \cap Q^{-1} [\{w\}]] = J^{-1} [Q^{-1} [\{w\}]]$
69		isocnv	$⊢ J {Isom}_{E, Q} (dom J, a \times a) \to J^{-1} {Isom}_{Q, E} (a \times a, dom J)$
70	47 69	syl	$⊢ (φ \land w \in (a \times a)) \to J^{-1} {Isom}_{Q, E} (a \times a, dom J)$
71		simpr	$⊢ (φ \land w \in (a \times a)) \to w \in (a \times a)$
72		isoini	$⊢ (J^{-1} {Isom}_{Q, E} (a \times a, dom J) \land w \in (a \times a)) \to J^{-1} [(a \times a) \cap Q^{-1} [\{w\}]] = dom J \cap E^{-1} [\{J^{-1} (w)\}]$
73	70 71 72	syl2anc	$⊢ (φ \land w \in (a \times a)) \to J^{-1} [(a \times a) \cap Q^{-1} [\{w\}]] = dom J \cap E^{-1} [\{J^{-1} (w)\}]$
74		fvex	$⊢ J^{-1} (w) \in V$
75	74	epini	$⊢ E^{-1} [\{J^{-1} (w)\}] = J^{-1} (w)$
76	75	ineq2i	$⊢ dom J \cap E^{-1} [\{J^{-1} (w)\}] = dom J \cap J^{-1} (w)$
77	6	oicl	$⊢ Ord dom J$
78		f1of	$⊢ J^{-1} : a \times a \underset{1-1 onto}{⟶} dom J \to J^{-1} : a \times a ⟶ dom J$
79	37 38 39 78	4syl	$⊢ φ \to J^{-1} : a \times a ⟶ dom J$
80	79	ffvelcdmda	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \in dom J$
81		ordelss	$⊢ (Ord dom J \land J^{-1} (w) \in dom J) \to J^{-1} (w) \subseteq dom J$
82	77 80 81	sylancr	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \subseteq dom J$
83		sseqin2	$⊢ J^{-1} (w) \subseteq dom J \leftrightarrow dom J \cap J^{-1} (w) = J^{-1} (w)$
84	82 83	sylib	$⊢ (φ \land w \in (a \times a)) \to dom J \cap J^{-1} (w) = J^{-1} (w)$
85	76 84	eqtrid	$⊢ (φ \land w \in (a \times a)) \to dom J \cap E^{-1} [\{J^{-1} (w)\}] = J^{-1} (w)$
86	73 85	eqtrd	$⊢ (φ \land w \in (a \times a)) \to J^{-1} [(a \times a) \cap Q^{-1} [\{w\}]] = J^{-1} (w)$
87	68 86	eqtr3id	$⊢ (φ \land w \in (a \times a)) \to J^{-1} [Q^{-1} [\{w\}]] = J^{-1} (w)$
88	65 87	breqtrd	$⊢ (φ \land w \in (a \times a)) \to Q^{-1} [\{w\}] \approx J^{-1} (w)$
89	88	ensymd	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \approx Q^{-1} [\{w\}]$
90		fvex	$⊢ 1^{st} (w) \in V$
91		fvex	$⊢ 2^{nd} (w) \in V$
92	90 91	unex	$⊢ 1^{st} (w) \cup 2^{nd} (w) \in V$
93	5 92	eqeltri	$⊢ M \in V$
94	93	sucex	$⊢ suc M \in V$
95	94 94	xpex	$⊢ suc M \times suc M \in V$
96		xpss	$⊢ a \times a \subseteq V \times V$
97		simp3	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to z \in Q^{-1} [\{w\}]$
98		vex	$⊢ z \in V$
99	98	eliniseg	$⊢ w \in V \to (z \in Q^{-1} [\{w\}] \leftrightarrow z Q w)$
100	99	elv	$⊢ z \in Q^{-1} [\{w\}] \leftrightarrow z Q w$
101	97 100	sylib	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to z Q w$
102	3	breqi	$⊢ z Q w \leftrightarrow z (R \cap ((a \times a) \times (a \times a))) w$
103		brin	$⊢ z (R \cap ((a \times a) \times (a \times a))) w \leftrightarrow (z R w \land z ((a \times a) \times (a \times a)) w)$
104	102 103	bitri	$⊢ z Q w \leftrightarrow (z R w \land z ((a \times a) \times (a \times a)) w)$
105	104	simprbi	$⊢ z Q w \to z ((a \times a) \times (a \times a)) w$
106		brxp	$⊢ z ((a \times a) \times (a \times a)) w \leftrightarrow (z \in (a \times a) \land w \in (a \times a))$
107	106	simplbi	$⊢ z ((a \times a) \times (a \times a)) w \to z \in (a \times a)$
108	101 105 107	3syl	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to z \in (a \times a)$
109	96 108	sselid	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to z \in (V \times V)$
110	22	adantr	$⊢ (φ \land w \in (a \times a)) \to a \in On$
111	110	3adant3	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to a \in On$
112		xp1st	$⊢ z \in (a \times a) \to 1^{st} (z) \in a$
113		onelon	$⊢ (a \in On \land 1^{st} (z) \in a) \to 1^{st} (z) \in On$
114	112 113	sylan2	$⊢ (a \in On \land z \in (a \times a)) \to 1^{st} (z) \in On$
115	111 108 114	syl2anc	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 1^{st} (z) \in On$
116		eloni	$⊢ a \in On \to Ord a$
117		elxp7	$⊢ w \in (a \times a) \leftrightarrow (w \in (V \times V) \land (1^{st} (w) \in a \land 2^{nd} (w) \in a))$
118	117	simprbi	$⊢ w \in (a \times a) \to (1^{st} (w) \in a \land 2^{nd} (w) \in a)$
119		ordunel	$⊢ (Ord a \land 1^{st} (w) \in a \land 2^{nd} (w) \in a) \to 1^{st} (w) \cup 2^{nd} (w) \in a$
120	119	3expib	$⊢ Ord a \to ((1^{st} (w) \in a \land 2^{nd} (w) \in a) \to 1^{st} (w) \cup 2^{nd} (w) \in a)$
121	116 118 120	syl2im	$⊢ a \in On \to (w \in (a \times a) \to 1^{st} (w) \cup 2^{nd} (w) \in a)$
122	110 71 121	sylc	$⊢ (φ \land w \in (a \times a)) \to 1^{st} (w) \cup 2^{nd} (w) \in a$
123	5 122	eqeltrid	$⊢ (φ \land w \in (a \times a)) \to M \in a$
124		simprr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to \forall m \in a m ≺ a$
125	4 124	sylbi	$⊢ φ \to \forall m \in a m ≺ a$
126		simprl	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to ω \subseteq a$
127	4 126	sylbi	$⊢ φ \to ω \subseteq a$
128		iscard	$⊢ card (a) = a \leftrightarrow (a \in On \land \forall m \in a m ≺ a)$
129		cardlim	$⊢ ω \subseteq card (a) \leftrightarrow Lim card (a)$
130		sseq2	$⊢ card (a) = a \to (ω \subseteq card (a) \leftrightarrow ω \subseteq a)$
131		limeq	$⊢ card (a) = a \to (Lim card (a) \leftrightarrow Lim a)$
132	130 131	bibi12d	$⊢ card (a) = a \to ((ω \subseteq card (a) \leftrightarrow Lim card (a)) \leftrightarrow (ω \subseteq a \leftrightarrow Lim a))$
133	129 132	mpbii	$⊢ card (a) = a \to (ω \subseteq a \leftrightarrow Lim a)$
134	128 133	sylbir	$⊢ (a \in On \land \forall m \in a m ≺ a) \to (ω \subseteq a \leftrightarrow Lim a)$
135	134	biimpa	$⊢ ((a \in On \land \forall m \in a m ≺ a) \land ω \subseteq a) \to Lim a$
136	22 125 127 135	syl21anc	$⊢ φ \to Lim a$
137	136	adantr	$⊢ (φ \land w \in (a \times a)) \to Lim a$
138		limsuc	$⊢ Lim a \to (M \in a \leftrightarrow suc M \in a)$
139	137 138	syl	$⊢ (φ \land w \in (a \times a)) \to (M \in a \leftrightarrow suc M \in a)$
140	123 139	mpbid	$⊢ (φ \land w \in (a \times a)) \to suc M \in a$
141		onelon	$⊢ (a \in On \land suc M \in a) \to suc M \in On$
142	22 140 141	syl2an2r	$⊢ (φ \land w \in (a \times a)) \to suc M \in On$
143	142	3adant3	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to suc M \in On$
144		ssun1	$⊢ 1^{st} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z)$
145	144	a1i	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 1^{st} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z)$
146	104	simplbi	$⊢ z Q w \to z R w$
147		df-br	$⊢ z R w \leftrightarrow ⟨z, w⟩ \in R$
148	2	eleq2i	$⊢ ⟨z, w⟩ \in R \leftrightarrow ⟨z, w⟩ \in \{⟨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)))\}$
149		opabidw	$⊢ ⟨z, w⟩ \in \{⟨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)))\} \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)))$
150	147 148 149	3bitri	$⊢ z R 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)))$
151	150	simprbi	$⊢ z R w \to (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))$
152		simpl	$⊢ (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z L w) \to 1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w)$
153	152	orim2i	$⊢ (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)) \to (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))$
154	151 153	syl	$⊢ z R w \to (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))$
155		fvex	$⊢ 1^{st} (z) \in V$
156		fvex	$⊢ 2^{nd} (z) \in V$
157	155 156	unex	$⊢ 1^{st} (z) \cup 2^{nd} (z) \in V$
158	157	elsuc	$⊢ 1^{st} (z) \cup 2^{nd} (z) \in suc (1^{st} (w) \cup 2^{nd} (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))$
159	154 158	sylibr	$⊢ z R w \to 1^{st} (z) \cup 2^{nd} (z) \in suc (1^{st} (w) \cup 2^{nd} (w))$
160		suceq	$⊢ M = 1^{st} (w) \cup 2^{nd} (w) \to suc M = suc (1^{st} (w) \cup 2^{nd} (w))$
161	5 160	ax-mp	$⊢ suc M = suc (1^{st} (w) \cup 2^{nd} (w))$
162	159 161	eleqtrrdi	$⊢ z R w \to 1^{st} (z) \cup 2^{nd} (z) \in suc M$
163	101 146 162	3syl	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 1^{st} (z) \cup 2^{nd} (z) \in suc M$
164		ontr2	$⊢ (1^{st} (z) \in On \land suc M \in On) \to ((1^{st} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z) \land 1^{st} (z) \cup 2^{nd} (z) \in suc M) \to 1^{st} (z) \in suc M)$
165	164	imp	$⊢ ((1^{st} (z) \in On \land suc M \in On) \land (1^{st} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z) \land 1^{st} (z) \cup 2^{nd} (z) \in suc M)) \to 1^{st} (z) \in suc M$
166	115 143 145 163 165	syl22anc	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 1^{st} (z) \in suc M$
167		xp2nd	$⊢ z \in (a \times a) \to 2^{nd} (z) \in a$
168		onelon	$⊢ (a \in On \land 2^{nd} (z) \in a) \to 2^{nd} (z) \in On$
169	167 168	sylan2	$⊢ (a \in On \land z \in (a \times a)) \to 2^{nd} (z) \in On$
170	111 108 169	syl2anc	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 2^{nd} (z) \in On$
171		ssun2	$⊢ 2^{nd} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z)$
172	171	a1i	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 2^{nd} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z)$
173		ontr2	$⊢ (2^{nd} (z) \in On \land suc M \in On) \to ((2^{nd} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z) \land 1^{st} (z) \cup 2^{nd} (z) \in suc M) \to 2^{nd} (z) \in suc M)$
174	173	imp	$⊢ ((2^{nd} (z) \in On \land suc M \in On) \land (2^{nd} (z) \subseteq 1^{st} (z) \cup 2^{nd} (z) \land 1^{st} (z) \cup 2^{nd} (z) \in suc M)) \to 2^{nd} (z) \in suc M$
175	170 143 172 163 174	syl22anc	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to 2^{nd} (z) \in suc M$
176		elxp7	$⊢ z \in (suc M \times suc M) \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in suc M \land 2^{nd} (z) \in suc M))$
177	176	biimpri	$⊢ (z \in (V \times V) \land (1^{st} (z) \in suc M \land 2^{nd} (z) \in suc M)) \to z \in (suc M \times suc M)$
178	109 166 175 177	syl12anc	$⊢ (φ \land w \in (a \times a) \land z \in Q^{-1} [\{w\}]) \to z \in (suc M \times suc M)$
179	178	3expia	$⊢ (φ \land w \in (a \times a)) \to (z \in Q^{-1} [\{w\}] \to z \in (suc M \times suc M))$
180	179	ssrdv	$⊢ (φ \land w \in (a \times a)) \to Q^{-1} [\{w\}] \subseteq suc M \times suc M$
181		ssdomg	$⊢ suc M \times suc M \in V \to (Q^{-1} [\{w\}] \subseteq suc M \times suc M \to Q^{-1} [\{w\}] ≼ (suc M \times suc M))$
182	95 180 181	mpsyl	$⊢ (φ \land w \in (a \times a)) \to Q^{-1} [\{w\}] ≼ (suc M \times suc M)$
183	127	adantr	$⊢ (φ \land w \in (a \times a)) \to ω \subseteq a$
184		nnfi	$⊢ suc M \in ω \to suc M \in Fin$
185		xpfi	$⊢ (suc M \in Fin \land suc M \in Fin) \to suc M \times suc M \in Fin$
186	185	anidms	$⊢ suc M \in Fin \to suc M \times suc M \in Fin$
187		isfinite	$⊢ suc M \times suc M \in Fin \leftrightarrow (suc M \times suc M) ≺ ω$
188	186 187	sylib	$⊢ suc M \in Fin \to (suc M \times suc M) ≺ ω$
189	184 188	syl	$⊢ suc M \in ω \to (suc M \times suc M) ≺ ω$
190		ssdomg	$⊢ a \in V \to (ω \subseteq a \to ω ≼ a)$
191	190	elv	$⊢ ω \subseteq a \to ω ≼ a$
192		sdomdomtr	$⊢ ((suc M \times suc M) ≺ ω \land ω ≼ a) \to (suc M \times suc M) ≺ a$
193	189 191 192	syl2an	$⊢ (suc M \in ω \land ω \subseteq a) \to (suc M \times suc M) ≺ a$
194	193	expcom	$⊢ ω \subseteq a \to (suc M \in ω \to (suc M \times suc M) ≺ a)$
195	183 194	syl	$⊢ (φ \land w \in (a \times a)) \to (suc M \in ω \to (suc M \times suc M) ≺ a)$
196		breq1	$⊢ m = suc M \to (m ≺ a \leftrightarrow suc M ≺ a)$
197	125	adantr	$⊢ (φ \land w \in (a \times a)) \to \forall m \in a m ≺ a$
198	196 197 140	rspcdva	$⊢ (φ \land w \in (a \times a)) \to suc M ≺ a$
199		omelon	$⊢ ω \in On$
200		ontri1	$⊢ (ω \in On \land suc M \in On) \to (ω \subseteq suc M \leftrightarrow \neg suc M \in ω)$
201	199 142 200	sylancr	$⊢ (φ \land w \in (a \times a)) \to (ω \subseteq suc M \leftrightarrow \neg suc M \in ω)$
202		sseq2	$⊢ m = suc M \to (ω \subseteq m \leftrightarrow ω \subseteq suc M)$
203		xpeq12	$⊢ (m = suc M \land m = suc M) \to m \times m = suc M \times suc M$
204	203	anidms	$⊢ m = suc M \to m \times m = suc M \times suc M$
205		id	$⊢ m = suc M \to m = suc M$
206	204 205	breq12d	$⊢ m = suc M \to ((m \times m) \approx m \leftrightarrow (suc M \times suc M) \approx suc M)$
207	202 206	imbi12d	$⊢ m = suc M \to ((ω \subseteq m \to (m \times m) \approx m) \leftrightarrow (ω \subseteq suc M \to (suc M \times suc M) \approx suc M))$
208		simplr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to \forall m \in a (ω \subseteq m \to (m \times m) \approx m)$
209	4 208	sylbi	$⊢ φ \to \forall m \in a (ω \subseteq m \to (m \times m) \approx m)$
210	209	adantr	$⊢ (φ \land w \in (a \times a)) \to \forall m \in a (ω \subseteq m \to (m \times m) \approx m)$
211	207 210 140	rspcdva	$⊢ (φ \land w \in (a \times a)) \to (ω \subseteq suc M \to (suc M \times suc M) \approx suc M)$
212	201 211	sylbird	$⊢ (φ \land w \in (a \times a)) \to (\neg suc M \in ω \to (suc M \times suc M) \approx suc M)$
213		ensdomtr	$⊢ ((suc M \times suc M) \approx suc M \land suc M ≺ a) \to (suc M \times suc M) ≺ a$
214	213	expcom	$⊢ suc M ≺ a \to ((suc M \times suc M) \approx suc M \to (suc M \times suc M) ≺ a)$
215	198 212 214	sylsyld	$⊢ (φ \land w \in (a \times a)) \to (\neg suc M \in ω \to (suc M \times suc M) ≺ a)$
216	195 215	pm2.61d	$⊢ (φ \land w \in (a \times a)) \to (suc M \times suc M) ≺ a$
217		domsdomtr	$⊢ (Q^{-1} [\{w\}] ≼ (suc M \times suc M) \land (suc M \times suc M) ≺ a) \to Q^{-1} [\{w\}] ≺ a$
218	182 216 217	syl2anc	$⊢ (φ \land w \in (a \times a)) \to Q^{-1} [\{w\}] ≺ a$
219		ensdomtr	$⊢ (J^{-1} (w) \approx Q^{-1} [\{w\}] \land Q^{-1} [\{w\}] ≺ a) \to J^{-1} (w) ≺ a$
220	89 218 219	syl2anc	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) ≺ a$
221		ordelon	$⊢ (Ord dom J \land J^{-1} (w) \in dom J) \to J^{-1} (w) \in On$
222	77 80 221	sylancr	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \in On$
223		onenon	$⊢ a \in On \to a \in dom card$
224	110 223	syl	$⊢ (φ \land w \in (a \times a)) \to a \in dom card$
225		cardsdomel	$⊢ (J^{-1} (w) \in On \land a \in dom card) \to (J^{-1} (w) ≺ a \leftrightarrow J^{-1} (w) \in card (a))$
226	222 224 225	syl2anc	$⊢ (φ \land w \in (a \times a)) \to (J^{-1} (w) ≺ a \leftrightarrow J^{-1} (w) \in card (a))$
227	220 226	mpbid	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \in card (a)$
228		eleq2	$⊢ card (a) = a \to (J^{-1} (w) \in card (a) \leftrightarrow J^{-1} (w) \in a)$
229	128 228	sylbir	$⊢ (a \in On \land \forall m \in a m ≺ a) \to (J^{-1} (w) \in card (a) \leftrightarrow J^{-1} (w) \in a)$
230	22 197 229	syl2an2r	$⊢ (φ \land w \in (a \times a)) \to (J^{-1} (w) \in card (a) \leftrightarrow J^{-1} (w) \in a)$
231	227 230	mpbid	$⊢ (φ \land w \in (a \times a)) \to J^{-1} (w) \in a$
232	231	ralrimiva	$⊢ φ \to \forall w \in (a \times a) J^{-1} (w) \in a$
233		fnfvrnss	$⊢ (J^{-1} Fn (a \times a) \land \forall w \in (a \times a) J^{-1} (w) \in a) \to ran J^{-1} \subseteq a$
234		ssdomg	$⊢ a \in V \to (ran J^{-1} \subseteq a \to ran J^{-1} ≼ a)$
235	19 233 234	mpsyl	$⊢ (J^{-1} Fn (a \times a) \land \forall w \in (a \times a) J^{-1} (w) \in a) \to ran J^{-1} ≼ a$
236	46 232 235	syl2anc	$⊢ φ \to ran J^{-1} ≼ a$
237		endomtr	$⊢ ((a \times a) \approx ran J^{-1} \land ran J^{-1} ≼ a) \to (a \times a) ≼ a$
238	44 236 237	syl2anc	$⊢ φ \to (a \times a) ≼ a$
239	4 238	sylbir	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to (a \times a) ≼ a$
240		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
241		1onn	$⊢ 1_{𝑜} \in ω$
242	240 241	eqeltrri	$⊢ \{\emptyset\} \in ω$
243		nnsdom	$⊢ \{\emptyset\} \in ω \to \{\emptyset\} ≺ ω$
244		sdomdom	$⊢ \{\emptyset\} ≺ ω \to \{\emptyset\} ≼ ω$
245	242 243 244	mp2b	$⊢ \{\emptyset\} ≼ ω$
246		domtr	$⊢ (\{\emptyset\} ≼ ω \land ω ≼ a) \to \{\emptyset\} ≼ a$
247	245 191 246	sylancr	$⊢ ω \subseteq a \to \{\emptyset\} ≼ a$
248		0ex	$⊢ \emptyset \in V$
249	19 248	xpsnen	$⊢ (a \times \{\emptyset\}) \approx a$
250	249	ensymi	$⊢ a \approx (a \times \{\emptyset\})$
251	19	xpdom2	$⊢ \{\emptyset\} ≼ a \to (a \times \{\emptyset\}) ≼ (a \times a)$
252		endomtr	$⊢ (a \approx (a \times \{\emptyset\}) \land (a \times \{\emptyset\}) ≼ (a \times a)) \to a ≼ (a \times a)$
253	250 251 252	sylancr	$⊢ \{\emptyset\} ≼ a \to a ≼ (a \times a)$
254	247 253	syl	$⊢ ω \subseteq a \to a ≼ (a \times a)$
255	254	ad2antrl	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to a ≼ (a \times a)$
256		sbth	$⊢ ((a \times a) ≼ a \land a ≼ (a \times a)) \to (a \times a) \approx a$
257	239 255 256	syl2anc	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \to (a \times a) \approx a$
258	257	expr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land ω \subseteq a) \to (\forall m \in a m ≺ a \to (a \times a) \approx a)$
259		simplr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to \forall m \in a (ω \subseteq m \to (m \times m) \approx m)$
260		simpll	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to a \in On$
261		simprr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to \neg \forall m \in a m ≺ a$
262		rexnal	$⊢ \exists m \in a \neg m ≺ a \leftrightarrow \neg \forall m \in a m ≺ a$
263		onelss	$⊢ a \in On \to (m \in a \to m \subseteq a)$
264		ssdomg	$⊢ a \in On \to (m \subseteq a \to m ≼ a)$
265	263 264	syld	$⊢ a \in On \to (m \in a \to m ≼ a)$
266		bren2	$⊢ m \approx a \leftrightarrow (m ≼ a \land \neg m ≺ a)$
267	266	simplbi2	$⊢ m ≼ a \to (\neg m ≺ a \to m \approx a)$
268	265 267	syl6	$⊢ a \in On \to (m \in a \to (\neg m ≺ a \to m \approx a))$
269	268	reximdvai	$⊢ a \in On \to (\exists m \in a \neg m ≺ a \to \exists m \in a m \approx a)$
270	262 269	biimtrrid	$⊢ a \in On \to (\neg \forall m \in a m ≺ a \to \exists m \in a m \approx a)$
271	260 261 270	sylc	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to \exists m \in a m \approx a$
272		r19.29	$⊢ (\forall m \in a (ω \subseteq m \to (m \times m) \approx m) \land \exists m \in a m \approx a) \to \exists m \in a ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a)$
273	259 271 272	syl2anc	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to \exists m \in a ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a)$
274		simprl	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to ω \subseteq a$
275		onelon	$⊢ (a \in On \land m \in a) \to m \in On$
276		ensym	$⊢ m \approx a \to a \approx m$
277		domentr	$⊢ (ω ≼ a \land a \approx m) \to ω ≼ m$
278	191 276 277	syl2an	$⊢ (ω \subseteq a \land m \approx a) \to ω ≼ m$
279		domnsym	$⊢ ω ≼ m \to \neg m ≺ ω$
280		nnsdom	$⊢ m \in ω \to m ≺ ω$
281	279 280	nsyl	$⊢ ω ≼ m \to \neg m \in ω$
282		ontri1	$⊢ (ω \in On \land m \in On) \to (ω \subseteq m \leftrightarrow \neg m \in ω)$
283	199 282	mpan	$⊢ m \in On \to (ω \subseteq m \leftrightarrow \neg m \in ω)$
284	281 283	imbitrrid	$⊢ m \in On \to (ω ≼ m \to ω \subseteq m)$
285	275 278 284	syl2im	$⊢ (a \in On \land m \in a) \to ((ω \subseteq a \land m \approx a) \to ω \subseteq m)$
286	285	expd	$⊢ (a \in On \land m \in a) \to (ω \subseteq a \to (m \approx a \to ω \subseteq m))$
287	286	impcom	$⊢ (ω \subseteq a \land (a \in On \land m \in a)) \to (m \approx a \to ω \subseteq m)$
288	287	imim1d	$⊢ (ω \subseteq a \land (a \in On \land m \in a)) \to ((ω \subseteq m \to (m \times m) \approx m) \to (m \approx a \to (m \times m) \approx m))$
289	288	imp32	$⊢ ((ω \subseteq a \land (a \in On \land m \in a)) \land ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a)) \to (m \times m) \approx m$
290		entr	$⊢ ((m \times m) \approx m \land m \approx a) \to (m \times m) \approx a$
291	290	ancoms	$⊢ (m \approx a \land (m \times m) \approx m) \to (m \times m) \approx a$
292		xpen	$⊢ (a \approx m \land a \approx m) \to (a \times a) \approx (m \times m)$
293	292	anidms	$⊢ a \approx m \to (a \times a) \approx (m \times m)$
294		entr	$⊢ ((a \times a) \approx (m \times m) \land (m \times m) \approx a) \to (a \times a) \approx a$
295	293 294	sylan	$⊢ (a \approx m \land (m \times m) \approx a) \to (a \times a) \approx a$
296	276 291 295	syl2an2r	$⊢ (m \approx a \land (m \times m) \approx m) \to (a \times a) \approx a$
297	296	ex	$⊢ m \approx a \to ((m \times m) \approx m \to (a \times a) \approx a)$
298	297	ad2antll	$⊢ ((ω \subseteq a \land (a \in On \land m \in a)) \land ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a)) \to ((m \times m) \approx m \to (a \times a) \approx a)$
299	289 298	mpd	$⊢ ((ω \subseteq a \land (a \in On \land m \in a)) \land ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a)) \to (a \times a) \approx a$
300	299	ex	$⊢ (ω \subseteq a \land (a \in On \land m \in a)) \to (((ω \subseteq m \to (m \times m) \approx m) \land m \approx a) \to (a \times a) \approx a)$
301	300	expr	$⊢ (ω \subseteq a \land a \in On) \to (m \in a \to (((ω \subseteq m \to (m \times m) \approx m) \land m \approx a) \to (a \times a) \approx a))$
302	301	rexlimdv	$⊢ (ω \subseteq a \land a \in On) \to (\exists m \in a ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a) \to (a \times a) \approx a)$
303	274 260 302	syl2anc	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to (\exists m \in a ((ω \subseteq m \to (m \times m) \approx m) \land m \approx a) \to (a \times a) \approx a)$
304	273 303	mpd	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \neg \forall m \in a m ≺ a)) \to (a \times a) \approx a$
305	304	expr	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land ω \subseteq a) \to (\neg \forall m \in a m ≺ a \to (a \times a) \approx a)$
306	258 305	pm2.61d	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land ω \subseteq a) \to (a \times a) \approx a$
307	306	exp31	$⊢ a \in On \to (\forall m \in a (ω \subseteq m \to (m \times m) \approx m) \to (ω \subseteq a \to (a \times a) \approx a))$
308	12 18 307	tfis3	$⊢ A \in On \to (ω \subseteq A \to (A \times A) \approx A)$
309	308	imp	$⊢ (A \in On \land ω \subseteq A) \to (A \times A) \approx A$

Metamath Proof Explorer

Theorem infxpenlem

Proof