Theorem infxpenlem 9973

Description: Lemma for infxpen 9974. (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 3976	. . . 4 ⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2		xpeq12 5666	. . . . . 6 ⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
3	2	anidms 566	. . . . 5 ⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4		id 22	. . . . 5 ⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚)
5	3, 4	breq12d 5123	. . . 4 ⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
6	1, 5	imbi12d 344	. . 3 ⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7		sseq2 3976	. . . 4 ⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8		xpeq12 5666	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
9	8	anidms 566	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10		id 22	. . . . 5 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
11	9, 10	breq12d 5123	. . . 4 ⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
12	7, 11	imbi12d 344	. . 3 ⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13		infxpen.2	. . . . . . . 8 ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
14		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
15	14, 14	xpex 7732	. . . . . . . . . . . 12 ⊢ (𝑎 × 𝑎) ∈ V
16		simpll 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
17	13, 16	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑎 ∈ On)
18		onss 7764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑎 ⊆ On)
20		xpss12 5656	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
21	19, 19, 20	syl2anc 584	. . . . . . . . . . . . . . 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 9972	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
25	24	simpli 483	. . . . . . . . . . . . . . 15 ⊢ 𝑅 We (On × On)
26		wess 5627	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎))
28		weinxp 5726	. . . . . . . . . . . . . 14 ⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
29	27, 28	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30		infxpen.1	. . . . . . . . . . . . . 14 ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31		weeq1 5628	. . . . . . . . . . . . . 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 9497	. . . . . . . . . . . 12 ⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
36	15, 33, 35	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37		isof1o 7301	. . . . . . . . . . 11 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎))
38		f1ocnv 6815	. . . . . . . . . . 11 ⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39		f1of1 6802	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41		f1f1orn 6814	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽)
42	15	f1oen 8947	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
44		f1ofn 6804	. . . . . . . . . . 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 6056	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄
49		inss2 4204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
50	30, 49	eqsstri 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51		dmss 5869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53		dmxpid 5897	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
54	52, 53	sseqtri 3998	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝑄 ⊆ (𝑎 × 𝑎)
55	48, 54	sstri 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56		f1ores 6817	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
57	47, 55, 56	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
58	15, 15	xpex 7732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
59	58	inex2 5276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
60	30, 59	eqeltri 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ∈ V
61	60	cnvex 7904	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡𝑄 ∈ V
62	61	imaex 7893	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ∈ V
63	62	f1oen 8947	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
64	46, 57, 63	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
65		sseqin2 4189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}))
66	55, 65	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})
67	66	imaeq2i 6032	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤}))
68		isocnv 7308	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71		isoini 7316	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
72	69, 70, 71	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
73		fvex 6874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐽‘𝑤) ∈ V
74	73	epini 6070	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤)
75	74	ineq2i 4183	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤))
76	34	oicl 9489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐽
77		f1of 6803	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
78	36, 37, 38, 77	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
79	78	ffvelcdmda 7059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽)
80		ordelss 6351	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
81	76, 79, 80	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
82		sseqin2 4189	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
83	81, 82	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
84	75, 83	eqtrid 2777	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤))
85	72, 84	eqtrd 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤))
86	67, 85	eqtr3id 2779	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤))
87	64, 86	breqtrd 5136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤))
88	87	ensymd 8979	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}))
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
90		fvex 6874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1st ‘𝑤) ∈ V
91		fvex 6874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘𝑤) ∈ V
92	90, 91	unex 7723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V
93	89, 92	eqeltri 2825	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ V
94	93	sucex 7785	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑀 ∈ V
95	94, 94	xpex 7732	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑀 × suc 𝑀) ∈ V
96		xpss 5657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 × 𝑎) ⊆ (V × V)
97		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤}))
98		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
99	98	eliniseg 6068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
100	99	elv 3455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
101	97, 100	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
102	30	breqi 5116	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
103		brin 5162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
104	102, 103	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105	104	simprbi 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
106		brxp 5690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
107	106	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎))
108	101, 105, 107	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
109	96, 108	sselid 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
110	17	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
111	110	3adant3 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On)
112		xp1st 8003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎)
113		onelon 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (1st ‘𝑧) ∈ 𝑎) → (1st ‘𝑧) ∈ On)
114	112, 113	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On)
115	111, 108, 114	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On)
116		eloni 6345	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ On → Ord 𝑎)
117		elxp7 8006	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)))
118	117	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎))
119		ordunel 7805	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . . . . . 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 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))
129		cardlim 9932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
130		sseq2 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
131		limeq 6347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
140	123, 139	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎)
141		onelon 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On)
142	17, 140, 141	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
143	142	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
144		ssun1 4144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
146	104	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤)
147		df-br 5111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
148	23	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))})
149		opabidw 5487	. . . . . . . . . . . . . . . . . . . . . . . . . 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 910	. . . . . . . . . . . . . . . . . . . . . . . 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 6874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1st ‘𝑧) ∈ V
156		fvex 6874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘𝑧) ∈ V
157	155, 156	unex 7723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V
158	157	elsuc 6407	. . . . . . . . . . . . . . . . . . . . . . 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 6403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
161	89, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤))
162	159, 161	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
163	101, 146, 162	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
164		ontr2 6383	. . . . . . . . . . . . . . . . . . . . 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 8004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎)
168		onelon 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (2nd ‘𝑧) ∈ 𝑎) → (2nd ‘𝑧) ∈ On)
169	167, 168	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On)
170	111, 108, 169	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On)
171		ssun2 4145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
173		ontr2 6383	. . . . . . . . . . . . . . . . . . . . 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 8006	. . . . . . . . . . . . . . . . . . . 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 3955	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
181		ssdomg 8974	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
182	95, 180, 181	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
183	127	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
184		nnfi 9137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
185		xpfi 9276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
186	185	anidms 566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
187		isfinite 9612	. . . . . . . . . . . . . . . . . . . . 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 8974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
191	190	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ⊆ 𝑎 → ω ≼ 𝑎)
192		sdomdomtr 9080	. . . . . . . . . . . . . . . . . . 19 ⊢ (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
193	189, 191, 192	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194	193	expcom 413	. . . . . . . . . . . . . . . . 17 ⊢ (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
195	183, 194	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196		breq1 5113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎))
197	125	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
198	196, 197, 140	rspcdva 3592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎)
199		omelon 9606	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
200		ontri1 6369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
201	199, 142, 200	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
202		sseq2 3976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
203		xpeq12 5666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
204	203	anidms 566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
205		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀)
206	204, 205	breq12d 5123	. . . . . . . . . . . . . . . . . . . 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 3592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212	201, 211	sylbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
213		ensdomtr 9083	. . . . . . . . . . . . . . . . . 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 9082	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
218	182, 216, 217	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
219		ensdomtr 9083	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎)
220	88, 218, 219	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎)
221		ordelon 6359	. . . . . . . . . . . . . . 15 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On)
222	76, 79, 221	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On)
223		onenon 9909	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ On → 𝑎 ∈ dom card)
224	110, 223	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
225		cardsdomel 9934	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
226	222, 224, 225	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
227	220, 226	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎))
228		eleq2 2818	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑎) = 𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
229	128, 228	sylbir 235	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
230	17, 197, 229	syl2an2r 685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
231	227, 230	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎)
232	231	ralrimiva 3126	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎)
233		fnfvrnss 7096	. . . . . . . . . . 11 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎)
234		ssdomg 8974	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎))
235	14, 233, 234	mpsyl 68	. . . . . . . . . 10 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎)
236	45, 232, 235	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎)
237		endomtr 8986	. . . . . . . . 9 ⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
238	43, 236, 237	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
239	13, 238	sylbir 235	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
240		df1o2 8444	. . . . . . . . . . . 12 ⊢ 1o = {∅}
241		1onn 8607	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
242	240, 241	eqeltrri 2826	. . . . . . . . . . 11 ⊢ {∅} ∈ ω
243		nnsdom 9614	. . . . . . . . . . 11 ⊢ ({∅} ∈ ω → {∅} ≺ ω)
244		sdomdom 8954	. . . . . . . . . . 11 ⊢ ({∅} ≺ ω → {∅} ≼ ω)
245	242, 243, 244	mp2b 10	. . . . . . . . . 10 ⊢ {∅} ≼ ω
246		domtr 8981	. . . . . . . . . 10 ⊢ (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
247	245, 191, 246	sylancr 587	. . . . . . . . 9 ⊢ (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
248		0ex 5265	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
249	14, 248	xpsnen 9029	. . . . . . . . . . 11 ⊢ (𝑎 × {∅}) ≈ 𝑎
250	249	ensymi 8978	. . . . . . . . . 10 ⊢ 𝑎 ≈ (𝑎 × {∅})
251	14	xpdom2 9041	. . . . . . . . . 10 ⊢ ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
252		endomtr 8986	. . . . . . . . . 10 ⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
253	250, 251, 252	sylancr 587	. . . . . . . . 9 ⊢ ({∅} ≼ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
254	247, 253	syl 17	. . . . . . . 8 ⊢ (ω ⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
255	254	ad2antrl 728	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256		sbth 9067	. . . . . . 7 ⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
257	239, 255, 256	syl2anc 584	. . . . . 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 3083	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
263		onelss 6377	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎))
264		ssdomg 8974	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎))
265	263, 264	syld 47	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎))
266		bren2 8957	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎))
267	266	simplbi2 500	. . . . . . . . . . . 12 ⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))
268	265, 267	syl6 35	. . . . . . . . . . 11 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)))
269	268	reximdvai 3145	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
270	262, 269	biimtrrid 243	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
271	260, 261, 270	sylc 65	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)
272		r19.29 3095	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
273	259, 271, 272	syl2anc 584	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
274		simprl 770	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
275		onelon 6360	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On)
276		ensym 8977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚)
277		domentr 8987	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚)
278	191, 276, 277	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚)
279		domnsym 9073	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
280		nnsdom 9614	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ω → 𝑚 ≺ ω)
281	279, 280	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
282		ontri1 6369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
283	199, 282	mpan 690	. . . . . . . . . . . . . . . . . 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 8980	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
291	290	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
292		xpen 9110	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
293	292	anidms 566	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
294		entr 8980	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
295	293, 294	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
296	276, 291, 295	syl2an2r 685	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
297	296	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
298	297	ad2antll 729	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
299	289, 298	mpd 15	. . . . . . . . . . 11 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
300	299	ex 412	. . . . . . . . . 10 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
301	300	expr 456	. . . . . . . . 9 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
302	301	rexlimdv 3133	. . . . . . . 8 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
303	274, 260, 302	syl2anc 584	. . . . . . 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 7837	. 2 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
309	308	imp 406	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  {csn 4592  ⟨cop 4598   class class class wbr 5110  {copab 5172   E cep 5540   Se wse 5592   We wwe 5593   × cxp 5639  ^◡ccnv 5640  dom cdm 5641  ran crn 5642   ↾ cres 5643   “ cima 5644  Ord word 6334  Oncon0 6335  Lim wlim 6336  suc csuc 6337   Fn wfn 6509  ⟶wf 6510  –1-1→wf1 6511  –1-1-onto→wf1o 6513  ‘cfv 6514   Isom wiso 6515  ωcom 7845  1^st c1st 7969  2^nd c2nd 7970  1_oc1o 8430   ≈ cen 8918   ≼ cdom 8919   ≺ csdm 8920  Fincfn 8921  OrdIsocoi 9469  cardccrd 9895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-oi 9470  df-card 9899

This theorem is referenced by:  infxpen  9974