Theorem infxpenlem 10017

Description: Lemma for infxpen 10018. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

Hypotheses

Ref	Expression
leweon.1	⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}
r0weon.1	⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))}
infxpen.1	⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
infxpen.2	⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
infxpen.3	⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
infxpen.4	⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))

Assertion

Ref	Expression
infxpenlem	⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Distinct variable groups:   𝐴,𝑎   𝑤,𝐽   𝑧,𝑤,𝐿   𝑧,𝑚,𝑀   𝜑,𝑤,𝑧   𝑧,𝑄   𝑚,𝑎,𝑤,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑚, 𝑎)   𝐴(𝑥, 𝑦, 𝑧, 𝑤, 𝑚)   𝑄(𝑥, 𝑦, 𝑤, 𝑚, 𝑎)   𝑅(𝑥, 𝑦, 𝑧, 𝑤, 𝑚, 𝑎)   𝐽(𝑥, 𝑦, 𝑧, 𝑚, 𝑎)   𝐿(𝑥, 𝑦, 𝑚, 𝑎)   𝑀(𝑥, 𝑦, 𝑤, 𝑎)

Proof of Theorem infxpenlem

Step	Hyp	Ref	Expression
1		sseq2 3957	. . . 4 ⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2		xpeq12 5680	. . . . . 6 ⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
3	2	anidms 577	. . . . 5 ⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4		id 23	. . . . 5 ⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚)
5	3, 4	breq12d 5116	. . . 4 ⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
6	1, 5	imbi12d 347	. . 3 ⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7		sseq2 3957	. . . 4 ⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8		xpeq12 5680	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
9	8	anidms 577	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10		id 23	. . . . 5 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
11	9, 10	breq12d 5116	. . . 4 ⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
12	7, 11	imbi12d 347	. . 3 ⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13		infxpen.2	. . . . . . . 8 ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
14		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
15	14, 14	xpex 7753	. . . . . . . . . . . 12 ⊢ (𝑎 × 𝑎) ∈ V
16		simpll 779	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
17	13, 16	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑎 ∈ On)
18		onss 7785	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
19	17, 18	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑎 ⊆ On)
20		xpss12 5670	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
21	19, 19, 20	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑎 × 𝑎) ⊆ (On × On))
22		leweon.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}
23		r0weon.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))}
24	22, 23	r0weon 10016	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
25	24	simpli 489	. . . . . . . . . . . . . . 15 ⊢ 𝑅 We (On × On)
26		wess 5641	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
27	21, 25, 26	mpisyl 22	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎))
28		weinxp 5740	. . . . . . . . . . . . . 14 ⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
29	27, 28	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30		infxpen.1	. . . . . . . . . . . . . 14 ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31		weeq1 5642	. . . . . . . . . . . . . 14 ⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
33	29, 32	sylibr 237	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎))
34		infxpen.4	. . . . . . . . . . . . 13 ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
35	34	oiiso 9510	. . . . . . . . . . . 12 ⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
36	15, 33, 35	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37		isof1o 7325	. . . . . . . . . . 11 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎))
38		f1ocnv 6831	. . . . . . . . . . 11 ⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39		f1of1 6817	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
40	36, 37, 38, 39	4syl 20	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41		f1f1orn 6830	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽)
42	15	f1oen 8979	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
43	40, 41, 42	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
44		f1ofn 6819	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽 Fn (𝑎 × 𝑎))
45	36, 37, 38, 44	4syl 20	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽 Fn (𝑎 × 𝑎))
46	36	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
47	37, 38, 39	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
48		cnvimass 6078	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄
49		inss2 4183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
50	30, 49	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51		dmss 5886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53		dmxpid 5914	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
54	52, 53	sseqtri 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝑄 ⊆ (𝑎 × 𝑎)
55	48, 54	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56		f1ores 6833	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
57	47, 55, 56	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
58	15, 15	xpex 7753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
59	58	inex2 5281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
60	30, 59	eqeltri 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ∈ V
61	60	cnvex 7923	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡𝑄 ∈ V
62	61	imaex 7912	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ∈ V
63	62	f1oen 8979	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
64	46, 57, 63	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
65		sseqin2 4169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}))
66	55, 65	mpbi 233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})
67	66	imaeq2i 6054	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤}))
68		isocnv 7332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
69	46, 68	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71		isoini 7340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
72	69, 70, 71	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
73		fvex 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐽‘𝑤) ∈ V
74	73	epini 6092	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤)
75	74	ineq2i 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤))
76	34	oicl 9502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐽
77		f1of 6818	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
78	36, 37, 38, 77	4syl 20	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
79	78	ffvelcdmda 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽)
80		ordelss 6373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
81	76, 79, 80	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
82		sseqin2 4169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
83	81, 82	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
84	75, 83	eqtrid 2807	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤))
85	72, 84	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤))
86	67, 85	eqtr3id 2809	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤))
87	64, 86	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤))
88	87	ensymd 9012	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}))
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
90		fvex 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1st ‘𝑤) ∈ V
91		fvex 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘𝑤) ∈ V
92	90, 91	unex 7747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V
93	89, 92	eqeltri 2856	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ V
94	93	sucex 7806	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑀 ∈ V
95	94, 94	xpex 7753	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑀 × suc 𝑀) ∈ V
96		xpss 5671	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 × 𝑎) ⊆ (V × V)
97		simp3 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤}))
98		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
99	98	eliniseg 6090	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
100	99	elv 3455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
101	97, 100	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
102	30	breqi 5109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
103		brin 5157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
104	102, 103	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105	104	simprbi 503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
106		brxp 5704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
107	106	simplbi 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎))
108	101, 105, 107	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
109	96, 108	sselid 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
110	17	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
111	110	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On)
112		xp1st 8019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎)
113		onelon 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (1st ‘𝑧) ∈ 𝑎) → (1st ‘𝑧) ∈ On)
114	112, 113	sylan2 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On)
115	111, 108, 114	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On)
116		eloni 6367	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ On → Ord 𝑎)
117		elxp7 8022	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)))
118	117	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎))
119		ordunel 7824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑎 ∧ (1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
120	119	3expib 1140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑎 → (((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
121	116, 118, 120	syl2im 41	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
122	110, 70, 121	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
123	89, 122	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎)
124		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
125	13, 124	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
126		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
127	13, 126	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ω ⊆ 𝑎)
128		iscard 9981	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))
129		cardlim 9978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
130		sseq2 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
131		limeq 6369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
132	130, 131	bibi12d 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
133	129, 132	mpbii 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
134	128, 133	sylbir 238	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135	134	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
136	17, 125, 127, 135	syl21anc 851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Lim 𝑎)
137	136	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
138		limsuc 7846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
139	137, 138	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
140	123, 139	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎)
141		onelon 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On)
142	17, 140, 141	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
143	142	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
144		ssun1 4124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
146	104	simplbi 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤)
147		df-br 5104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
148	23	eleq2i 2852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))})
149		opabidw 5502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))} ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))))
150	147, 148, 149	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))))
151	150	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))
152		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
153	152	orim2i 924	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
154	151, 153	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
155		fvex 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1st ‘𝑧) ∈ V
156		fvex 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘𝑧) ∈ V
157	155, 156	unex 7747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V
158	157	elsuc 6430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
159	154, 158	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
160		suceq 6426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
161	89, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤))
162	159, 161	eleqtrrdi 2871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
163	101, 146, 162	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
164		ontr2 6406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (1st ‘𝑧) ∈ suc 𝑀))
165	164	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (1st ‘𝑧) ∈ suc 𝑀)
166	115, 143, 145, 163, 165	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀)
167		xp2nd 8020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎)
168		onelon 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (2nd ‘𝑧) ∈ 𝑎) → (2nd ‘𝑧) ∈ On)
169	167, 168	sylan2 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On)
170	111, 108, 169	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On)
171		ssun2 4125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
173		ontr2 6406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (2nd ‘𝑧) ∈ suc 𝑀))
174	173	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (2nd ‘𝑧) ∈ suc 𝑀)
175	170, 143, 172, 163, 174	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀)
176		elxp7 8022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)))
177	176	biimpri 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
178	109, 166, 175, 177	syl12anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179	178	3expia 1139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
180	179	ssrdv 3937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
181		ssdomg 9007	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
182	95, 180, 181	mpsyl 69	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
183	127	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
184		nnfi 9163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
185		xpfi 9290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
186	185	anidms 577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
187		isfinite 9632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
188	186, 187	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
189	184, 188	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
190		ssdomg 9007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
191	190	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ⊆ 𝑎 → ω ≼ 𝑎)
192		sdomdomtr 9109	. . . . . . . . . . . . . . . . . . 19 ⊢ (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
193	189, 191, 192	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194	193	expcom 419	. . . . . . . . . . . . . . . . 17 ⊢ (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
195	183, 194	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196		breq1 5106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎))
197	125	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
198	196, 197, 140	rspcdva 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎)
199		omelon 9626	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
200		ontri1 6392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
201	199, 142, 200	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
202		sseq2 3957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
203		xpeq12 5680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
204	203	anidms 577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
205		id 23	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀)
206	204, 205	breq12d 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
207	202, 206	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
208		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
209	13, 208	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
210	209	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
211	207, 210, 140	rspcdva 3577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212	201, 211	sylbird 263	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
213		ensdomtr 9112	. . . . . . . . . . . . . . . . . 18 ⊢ (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
214	213	expcom 419	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
215	198, 212, 214	sylsyld 62	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
216	195, 215	pm2.61d 181	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
217		domsdomtr 9111	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
218	182, 216, 217	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
219		ensdomtr 9112	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎)
220	88, 218, 219	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎)
221		ordelon 6381	. . . . . . . . . . . . . . 15 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On)
222	76, 79, 221	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On)
223		onenon 9955	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ On → 𝑎 ∈ dom card)
224	110, 223	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
225		cardsdomel 9980	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
226	222, 224, 225	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
227	220, 226	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎))
228		eleq2 2849	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑎) = 𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
229	128, 228	sylbir 238	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
230	17, 197, 229	syl2an2r 698	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
231	227, 230	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎)
232	231	ralrimiva 3154	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎)
233		fnfvrnss 7115	. . . . . . . . . . 11 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎)
234		ssdomg 9007	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎))
235	14, 233, 234	mpsyl 69	. . . . . . . . . 10 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎)
236	45, 232, 235	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎)
237		endomtr 9019	. . . . . . . . 9 ⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
238	43, 236, 237	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
239	13, 238	sylbir 238	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
240		df1o2 8463	. . . . . . . . . . . 12 ⊢ 1o = {∅}
241		1onn 8629	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
242	240, 241	eqeltrri 2857	. . . . . . . . . . 11 ⊢ {∅} ∈ ω
243		nnsdom 9634	. . . . . . . . . . 11 ⊢ ({∅} ∈ ω → {∅} ≺ ω)
244		sdomdom 8987	. . . . . . . . . . 11 ⊢ ({∅} ≺ ω → {∅} ≼ ω)
245	242, 243, 244	mp2b 10	. . . . . . . . . 10 ⊢ {∅} ≼ ω
246		domtr 9014	. . . . . . . . . 10 ⊢ (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
247	245, 191, 246	sylancr 599	. . . . . . . . 9 ⊢ (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
248		0ex 5264	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
249	14, 248	xpsnen 9060	. . . . . . . . . . 11 ⊢ (𝑎 × {∅}) ≈ 𝑎
250	249	ensymi 9011	. . . . . . . . . 10 ⊢ 𝑎 ≈ (𝑎 × {∅})
251	14	xpdom2 9071	. . . . . . . . . 10 ⊢ ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
252		endomtr 9019	. . . . . . . . . 10 ⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
253	250, 251, 252	sylancr 599	. . . . . . . . 9 ⊢ ({∅} ≼ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
254	247, 253	syl 18	. . . . . . . 8 ⊢ (ω ⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
255	254	ad2antrl 741	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256		sbth 9096	. . . . . . 7 ⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
257	239, 255, 256	syl2anc 596	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
258	257	expr 462	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
259		simplr 781	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
260		simpll 779	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
261		simprr 785	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
262		rexnal 3114	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
263		onelss 6400	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎))
264		ssdomg 9007	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎))
265	263, 264	syld 48	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎))
266		bren2 8990	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎))
267	266	simplbi2 506	. . . . . . . . . . . 12 ⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))
268	265, 267	syl6 36	. . . . . . . . . . 11 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)))
269	268	reximdvai 3173	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
270	262, 269	biimtrrid 246	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
271	260, 261, 270	sylc 66	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)
272		r19.29 3125	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
273	259, 271, 272	syl2anc 596	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
274		simprl 783	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
275		onelon 6382	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On)
276		ensym 9010	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚)
277		domentr 9020	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚)
278	191, 276, 277	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚)
279		domnsym 9102	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
280		nnsdom 9634	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ω → 𝑚 ≺ ω)
281	279, 280	nsyl 141	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
282		ontri1 6392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
283	199, 282	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
284	281, 283	imbitrrid 249	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
285	275, 278, 284	syl2im 41	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚))
286	285	expd 421	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)))
287	286	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))
288	287	imim1d 83	. . . . . . . . . . . . 13 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
289	288	imp32 424	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
290		entr 9013	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
291	290	ancoms 464	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
292		xpen 9139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
293	292	anidms 577	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
294		entr 9013	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
295	293, 294	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
296	276, 291, 295	syl2an2r 698	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
297	296	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
298	297	ad2antll 742	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
299	289, 298	mpd 16	. . . . . . . . . . 11 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
300	299	ex 418	. . . . . . . . . 10 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
301	300	expr 462	. . . . . . . . 9 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
302	301	rexlimdv 3161	. . . . . . . 8 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
303	274, 260, 302	syl2anc 596	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304	273, 303	mpd 16	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
305	304	expr 462	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
306	258, 305	pm2.61d 181	. . . 4 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
307	306	exp31 425	. . 3 ⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
308	6, 12, 307	tfis3 7855	. 2 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
309	308	imp 412	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {csn 4584  ⟨cop 4590   class class class wbr 5103  {copab 5167   E cep 5554   Se wse 5606   We wwe 5607   × cxp 5653  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   ↾ cres 5657   “ cima 5658  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359   Fn wfn 6528  ⟶wf 6529  –1-1→wf1 6530  –1-1-onto→wf1o 6532  ‘cfv 6533   Isom wiso 6534  ωcom 7863  1^st c1st 7985  2^nd c2nd 7986  1_oc1o 8449   ≈ cen 8950   ≼ cdom 8951   ≺ csdm 8952  Fincfn 8953  OrdIsocoi 9482  cardccrd 9941

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-inf2 9621

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-oi 9483  df-card 9945

This theorem is used by:  infxpen  10018