Theorem infxpenlem 10082

Description: Lemma for infxpen 10083. (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 4035	. . . 4 ⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2		xpeq12 5725	. . . . . 6 ⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
3	2	anidms 566	. . . . 5 ⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4		id 22	. . . . 5 ⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚)
5	3, 4	breq12d 5179	. . . 4 ⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
6	1, 5	imbi12d 344	. . 3 ⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7		sseq2 4035	. . . 4 ⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8		xpeq12 5725	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
9	8	anidms 566	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10		id 22	. . . . 5 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
11	9, 10	breq12d 5179	. . . 4 ⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
12	7, 11	imbi12d 344	. . 3 ⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13		infxpen.2	. . . . . . . 8 ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
14		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
15	14, 14	xpex 7788	. . . . . . . . . . . 12 ⊢ (𝑎 × 𝑎) ∈ V
16		simpll 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
17	13, 16	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑎 ∈ On)
18		onss 7820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑎 ⊆ On)
20		xpss12 5715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
21	19, 19, 20	syl2anc 583	. . . . . . . . . . . . . . 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 10081	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
25	24	simpli 483	. . . . . . . . . . . . . . 15 ⊢ 𝑅 We (On × On)
26		wess 5686	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎))
28		weinxp 5784	. . . . . . . . . . . . . 14 ⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
29	27, 28	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30		infxpen.1	. . . . . . . . . . . . . 14 ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31		weeq1 5687	. . . . . . . . . . . . . 14 ⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
33	29, 32	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎))
34		infxpen.4	. . . . . . . . . . . . 13 ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
35	34	oiiso 9606	. . . . . . . . . . . 12 ⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
36	15, 33, 35	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37		isof1o 7359	. . . . . . . . . . 11 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎))
38		f1ocnv 6874	. . . . . . . . . . 11 ⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39		f1of1 6861	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41		f1f1orn 6873	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽)
42	15	f1oen 9033	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
44		f1ofn 6863	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽 Fn (𝑎 × 𝑎))
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽 Fn (𝑎 × 𝑎))
46	36	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
48		cnvimass 6111	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄
49		inss2 4259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
50	30, 49	eqsstri 4043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51		dmss 5927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53		dmxpid 5955	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
54	52, 53	sseqtri 4045	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝑄 ⊆ (𝑎 × 𝑎)
55	48, 54	sstri 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56		f1ores 6876	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
57	47, 55, 56	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
58	15, 15	xpex 7788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
59	58	inex2 5336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
60	30, 59	eqeltri 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ∈ V
61	60	cnvex 7965	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡𝑄 ∈ V
62	61	imaex 7954	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ∈ V
63	62	f1oen 9033	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
64	46, 57, 63	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
65		sseqin2 4244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}))
66	55, 65	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})
67	66	imaeq2i 6087	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤}))
68		isocnv 7366	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71		isoini 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
72	69, 70, 71	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
73		fvex 6933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐽‘𝑤) ∈ V
74	73	epini 6126	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤)
75	74	ineq2i 4238	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤))
76	34	oicl 9598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐽
77		f1of 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
78	36, 37, 38, 77	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
79	78	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽)
80		ordelss 6411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
81	76, 79, 80	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
82		sseqin2 4244	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
83	81, 82	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
84	75, 83	eqtrid 2792	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤))
85	72, 84	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤))
86	67, 85	eqtr3id 2794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤))
87	64, 86	breqtrd 5192	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤))
88	87	ensymd 9065	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}))
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
90		fvex 6933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1st ‘𝑤) ∈ V
91		fvex 6933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘𝑤) ∈ V
92	90, 91	unex 7779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V
93	89, 92	eqeltri 2840	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ V
94	93	sucex 7842	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑀 ∈ V
95	94, 94	xpex 7788	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑀 × suc 𝑀) ∈ V
96		xpss 5716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 × 𝑎) ⊆ (V × V)
97		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤}))
98		vex 3492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
99	98	eliniseg 6124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
100	99	elv 3493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
101	97, 100	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
102	30	breqi 5172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
103		brin 5218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
104	102, 103	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105	104	simprbi 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
106		brxp 5749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
107	106	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎))
108	101, 105, 107	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
109	96, 108	sselid 4006	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
110	17	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
111	110	3adant3 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On)
112		xp1st 8062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎)
113		onelon 6420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (1st ‘𝑧) ∈ 𝑎) → (1st ‘𝑧) ∈ On)
114	112, 113	sylan2 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On)
115	111, 108, 114	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On)
116		eloni 6405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ On → Ord 𝑎)
117		elxp7 8065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)))
118	117	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎))
119		ordunel 7863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑎 ∧ (1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
120	119	3expib 1122	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑎 → (((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
121	116, 118, 120	syl2im 40	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
122	110, 70, 121	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
123	89, 122	eqeltrid 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎)
124		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
125	13, 124	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
126		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
127	13, 126	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ω ⊆ 𝑎)
128		iscard 10044	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))
129		cardlim 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
130		sseq2 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
131		limeq 6407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
132	130, 131	bibi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
133	129, 132	mpbii 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
134	128, 133	sylbir 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135	134	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
136	17, 125, 127, 135	syl21anc 837	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Lim 𝑎)
137	136	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
138		limsuc 7886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
140	123, 139	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎)
141		onelon 6420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On)
142	17, 140, 141	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
143	142	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
144		ssun1 4201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
146	104	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤)
147		df-br 5167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
148	23	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))})
149		opabidw 5543	. . . . . . . . . . . . . . . . . . . . . . . . . 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 297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))))
151	150	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))
152		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
153	152	orim2i 909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
154	151, 153	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
155		fvex 6933	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1st ‘𝑧) ∈ V
156		fvex 6933	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘𝑧) ∈ V
157	155, 156	unex 7779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V
158	157	elsuc 6465	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
159	154, 158	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
160		suceq 6461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
161	89, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤))
162	159, 161	eleqtrrdi 2855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
163	101, 146, 162	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
164		ontr2 6442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (1st ‘𝑧) ∈ suc 𝑀))
165	164	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (1st ‘𝑧) ∈ suc 𝑀)
166	115, 143, 145, 163, 165	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀)
167		xp2nd 8063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎)
168		onelon 6420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (2nd ‘𝑧) ∈ 𝑎) → (2nd ‘𝑧) ∈ On)
169	167, 168	sylan2 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On)
170	111, 108, 169	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On)
171		ssun2 4202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
173		ontr2 6442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (2nd ‘𝑧) ∈ suc 𝑀))
174	173	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (2nd ‘𝑧) ∈ suc 𝑀)
175	170, 143, 172, 163, 174	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀)
176		elxp7 8065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)))
177	176	biimpri 228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
178	109, 166, 175, 177	syl12anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179	178	3expia 1121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
180	179	ssrdv 4014	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
181		ssdomg 9060	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
182	95, 180, 181	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
183	127	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
184		nnfi 9233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
185		xpfi 9386	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
186	185	anidms 566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
187		isfinite 9721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
188	186, 187	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
189	184, 188	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
190		ssdomg 9060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
191	190	elv 3493	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ⊆ 𝑎 → ω ≼ 𝑎)
192		sdomdomtr 9176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
193	189, 191, 192	syl2an 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194	193	expcom 413	. . . . . . . . . . . . . . . . 17 ⊢ (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
195	183, 194	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196		breq1 5169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎))
197	125	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
198	196, 197, 140	rspcdva 3636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎)
199		omelon 9715	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
200		ontri1 6429	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
201	199, 142, 200	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
202		sseq2 4035	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
203		xpeq12 5725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
204	203	anidms 566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
205		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀)
206	204, 205	breq12d 5179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
207	202, 206	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
208		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
209	13, 208	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
210	209	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
211	207, 210, 140	rspcdva 3636	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212	201, 211	sylbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
213		ensdomtr 9179	. . . . . . . . . . . . . . . . . 18 ⊢ (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
214	213	expcom 413	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
215	198, 212, 214	sylsyld 61	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
216	195, 215	pm2.61d 179	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
217		domsdomtr 9178	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
218	182, 216, 217	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
219		ensdomtr 9179	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎)
220	88, 218, 219	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎)
221		ordelon 6419	. . . . . . . . . . . . . . 15 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On)
222	76, 79, 221	sylancr 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On)
223		onenon 10018	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ On → 𝑎 ∈ dom card)
224	110, 223	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
225		cardsdomel 10043	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
226	222, 224, 225	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
227	220, 226	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎))
228		eleq2 2833	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑎) = 𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
229	128, 228	sylbir 235	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
230	17, 197, 229	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
231	227, 230	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎)
232	231	ralrimiva 3152	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎)
233		fnfvrnss 7155	. . . . . . . . . . 11 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎)
234		ssdomg 9060	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎))
235	14, 233, 234	mpsyl 68	. . . . . . . . . 10 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎)
236	45, 232, 235	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎)
237		endomtr 9072	. . . . . . . . 9 ⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
238	43, 236, 237	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
239	13, 238	sylbir 235	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
240		df1o2 8529	. . . . . . . . . . . 12 ⊢ 1o = {∅}
241		1onn 8696	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
242	240, 241	eqeltrri 2841	. . . . . . . . . . 11 ⊢ {∅} ∈ ω
243		nnsdom 9723	. . . . . . . . . . 11 ⊢ ({∅} ∈ ω → {∅} ≺ ω)
244		sdomdom 9040	. . . . . . . . . . 11 ⊢ ({∅} ≺ ω → {∅} ≼ ω)
245	242, 243, 244	mp2b 10	. . . . . . . . . 10 ⊢ {∅} ≼ ω
246		domtr 9067	. . . . . . . . . 10 ⊢ (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
247	245, 191, 246	sylancr 586	. . . . . . . . 9 ⊢ (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
248		0ex 5325	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
249	14, 248	xpsnen 9121	. . . . . . . . . . 11 ⊢ (𝑎 × {∅}) ≈ 𝑎
250	249	ensymi 9064	. . . . . . . . . 10 ⊢ 𝑎 ≈ (𝑎 × {∅})
251	14	xpdom2 9133	. . . . . . . . . 10 ⊢ ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
252		endomtr 9072	. . . . . . . . . 10 ⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
253	250, 251, 252	sylancr 586	. . . . . . . . 9 ⊢ ({∅} ≼ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
254	247, 253	syl 17	. . . . . . . 8 ⊢ (ω ⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
255	254	ad2antrl 727	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256		sbth 9159	. . . . . . 7 ⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
257	239, 255, 256	syl2anc 583	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
258	257	expr 456	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
259		simplr 768	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
260		simpll 766	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
261		simprr 772	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
262		rexnal 3106	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
263		onelss 6437	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎))
264		ssdomg 9060	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎))
265	263, 264	syld 47	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎))
266		bren2 9043	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎))
267	266	simplbi2 500	. . . . . . . . . . . 12 ⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))
268	265, 267	syl6 35	. . . . . . . . . . 11 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)))
269	268	reximdvai 3171	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
270	262, 269	biimtrrid 243	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
271	260, 261, 270	sylc 65	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)
272		r19.29 3120	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
273	259, 271, 272	syl2anc 583	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
274		simprl 770	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
275		onelon 6420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On)
276		ensym 9063	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚)
277		domentr 9073	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚)
278	191, 276, 277	syl2an 595	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚)
279		domnsym 9165	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
280		nnsdom 9723	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ω → 𝑚 ≺ ω)
281	279, 280	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
282		ontri1 6429	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
283	199, 282	mpan 689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
284	281, 283	imbitrrid 246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
285	275, 278, 284	syl2im 40	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚))
286	285	expd 415	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)))
287	286	impcom 407	. . . . . . . . . . . . . 14 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))
288	287	imim1d 82	. . . . . . . . . . . . 13 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
289	288	imp32 418	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
290		entr 9066	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
291	290	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
292		xpen 9206	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
293	292	anidms 566	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
294		entr 9066	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
295	293, 294	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
296	276, 291, 295	syl2an2r 684	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
297	296	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
298	297	ad2antll 728	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
299	289, 298	mpd 15	. . . . . . . . . . 11 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
300	299	ex 412	. . . . . . . . . 10 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
301	300	expr 456	. . . . . . . . 9 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
302	301	rexlimdv 3159	. . . . . . . 8 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
303	274, 260, 302	syl2anc 583	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304	273, 303	mpd 15	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
305	304	expr 456	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
306	258, 305	pm2.61d 179	. . . 4 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
307	306	exp31 419	. . 3 ⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
308	6, 12, 307	tfis3 7895	. 2 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
309	308	imp 406	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648  ⟨cop 4654   class class class wbr 5166  {copab 5228   E cep 5598   Se wse 5650   We wwe 5651   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701   ↾ cres 5702   “ cima 5703  Ord word 6394  Oncon0 6395  Lim wlim 6396  suc csuc 6397   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –1-1-onto→wf1o 6572  ‘cfv 6573   Isom wiso 6574  ωcom 7903  1^st c1st 8028  2^nd c2nd 8029  1_oc1o 8515   ≈ cen 9000   ≼ cdom 9001   ≺ csdm 9002  Fincfn 9003  OrdIsocoi 9578  cardccrd 10004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-oi 9579  df-card 10008

This theorem is referenced by:  infxpen  10083