Theorem infxpenlem 8719

Description: Lemma for infxpen 8720. (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 3590	. . . 4 ⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2		xpeq12 5058	. . . . . 6 ⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
3	2	anidms 675	. . . . 5 ⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4		id 22	. . . . 5 ⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚)
5	3, 4	breq12d 4596	. . . 4 ⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
6	1, 5	imbi12d 333	. . 3 ⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7		sseq2 3590	. . . 4 ⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8		xpeq12 5058	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
9	8	anidms 675	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10		id 22	. . . . 5 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
11	9, 10	breq12d 4596	. . . 4 ⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
12	7, 11	imbi12d 333	. . 3 ⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13		infxpen.2	. . . . . . . 8 ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
14		vex 3176	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
15	14, 14	xpex 6860	. . . . . . . . . . . 12 ⊢ (𝑎 × 𝑎) ∈ V
16		simpll 786	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
17	13, 16	sylbi 206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑎 ∈ On)
18		onss 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑎 ⊆ On)
20		xpss12 5148	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ⊆ On) → (𝑎 × 𝑎) ⊆ (On × On))
21	19, 19, 20	syl2anc 691	. . . . . . . . . . . . . . 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 8718	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
25	24	simpli 473	. . . . . . . . . . . . . . 15 ⊢ 𝑅 We (On × On)
26		wess 5025	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎))
28		weinxp 5109	. . . . . . . . . . . . . 14 ⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
29	27, 28	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30		infxpen.1	. . . . . . . . . . . . . 14 ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31		weeq1 5026	. . . . . . . . . . . . . 14 ⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
33	29, 32	sylibr 223	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎))
34		infxpen.4	. . . . . . . . . . . . 13 ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
35	34	oiiso 8325	. . . . . . . . . . . 12 ⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
36	15, 33, 35	sylancr 694	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37		isof1o 6473	. . . . . . . . . . 11 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎))
38		f1ocnv 6062	. . . . . . . . . . 11 ⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39		f1of1 6049	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41		f1f1orn 6061	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽)
42	15	f1oen 7862	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
44		f1ofn 6051	. . . . . . . . . . 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 5404	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄
49		inss2 3796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
50	30, 49	eqsstri 3598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51		dmss 5245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53		dmxpid 5266	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
54	52, 53	sseqtri 3600	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝑄 ⊆ (𝑎 × 𝑎)
55	48, 54	sstri 3577	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56		f1ores 6064	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
57	47, 55, 56	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
58	15, 15	xpex 6860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
59	58	inex2 4728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
60	30, 59	eqeltri 2684	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ∈ V
61	60	cnvex 7006	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡𝑄 ∈ V
62	61	imaex 6996	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ∈ V
63	62	f1oen 7862	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
64	46, 57, 63	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
65		sseqin2 3779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}))
66	55, 65	mpbi 219	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})
67	66	imaeq2i 5383	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤}))
68		isocnv 6480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70		simpr 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71		isoini 6488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
72	69, 70, 71	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
73		fvex 6113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐽‘𝑤) ∈ V
74	73	epini 5414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤)
75	74	ineq2i 3773	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤))
76	34	oicl 8317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐽
77		f1of 6050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
78	36, 37, 38, 77	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
79	78	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽)
80		ordelss 5656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
81	76, 79, 80	sylancr 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
82		sseqin2 3779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
83	81, 82	sylib 207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
84	75, 83	syl5eq 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤))
85	72, 84	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤))
86	67, 85	syl5eqr 2658	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤))
87	64, 86	breqtrd 4609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤))
88	87	ensymd 7893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}))
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
90		fvex 6113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1st ‘𝑤) ∈ V
91		fvex 6113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘𝑤) ∈ V
92	90, 91	unex 6854	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V
93	89, 92	eqeltri 2684	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ V
94	93	sucex 6903	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑀 ∈ V
95	94, 94	xpex 6860	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑀 × suc 𝑀) ∈ V
96		xpss 5149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 × 𝑎) ⊆ (V × V)
97		simp3 1056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤}))
98		vex 3176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
99		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
100	99	eliniseg 5413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
101	98, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
102	97, 101	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
103	30	breqi 4589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
104		brin 4634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105	103, 104	bitri 263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
106	105	simprbi 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
107		brxp 5071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
108	107	simplbi 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎))
109	102, 106, 108	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
110	96, 109	sseldi 3566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
111	17	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
112	111	3adant3 1074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On)
113		xp1st 7089	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎)
114		onelon 5665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (1st ‘𝑧) ∈ 𝑎) → (1st ‘𝑧) ∈ On)
115	113, 114	sylan2 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (1st ‘𝑧) ∈ On)
116	112, 109, 115	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ On)
117		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ On → Ord 𝑎)
118		elxp7 7092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)))
119	118	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎))
120		ordunel 6919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑎 ∧ (1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
121	120	3expib 1260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑎 → (((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
122	117, 119, 121	syl2im 39	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ On → (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎))
123	111, 70, 122	sylc 63	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
124	89, 123	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎)
125		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
126	13, 125	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
127		simprl 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
128	13, 127	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ω ⊆ 𝑎)
129		iscard 8684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))
130		cardlim 8681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
131		sseq2 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
132		limeq 5652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
133	131, 132	bibi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
134	130, 133	mpbii 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135	129, 134	sylbir 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
136	135	biimpa 500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
137	17, 126, 128, 136	syl21anc 1317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Lim 𝑎)
138	137	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
139		limsuc 6941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
140	138, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
141	124, 140	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎)
142		onelon 5665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On)
143	17, 141, 142	syl2an2r 872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
144	143	3adant3 1074	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
145		ssun1 3738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
146	145	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
147	105	simplbi 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤)
148		df-br 4584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
149	23	eleq2i 2680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))})
150		opabid 4907	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ‘𝑤)) ∧ 𝑧𝐿𝑤))))
151	148, 149, 150	3bitri 285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧𝑅𝑤 ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤))))
152	151	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))
153		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
154	153	orim2i 539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
155	152, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
156		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1st ‘𝑧) ∈ V
157		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘𝑧) ∈ V
158	156, 157	unex 6854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V
159	158	elsuc 5711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
160	155, 159	sylibr 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
161		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
162	89, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤))
163	160, 162	syl6eleqr 2699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
164	102, 147, 163	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
165		ontr2 5689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (1st ‘𝑧) ∈ suc 𝑀))
166	165	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (1st ‘𝑧) ∈ suc 𝑀)
167	116, 144, 146, 164, 166	syl22anc 1319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀)
168		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎)
169		onelon 5665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ (2nd ‘𝑧) ∈ 𝑎) → (2nd ‘𝑧) ∈ On)
170	168, 169	sylan2 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ (𝑎 × 𝑎)) → (2nd ‘𝑧) ∈ On)
171	112, 109, 170	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ On)
172		ssun2 3739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
174		ontr2 5689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (2nd ‘𝑧) ∈ suc 𝑀))
175	174	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (2nd ‘𝑧) ∈ suc 𝑀)
176	171, 144, 173, 164, 175	syl22anc 1319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀)
177		elxp7 7092	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)))
178	177	biimpri 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179	110, 167, 176, 178	syl12anc 1316	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
180	179	3expia 1259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
181	180	ssrdv 3574	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
182		ssdomg 7887	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
183	95, 181, 182	mpsyl 66	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
184	128	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
185		nnfi 8038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
186		xpfi 8116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
187	186	anidms 675	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
188		isfinite 8432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
189	187, 188	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
190	185, 189	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
191		ssdomg 7887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
192	14, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ⊆ 𝑎 → ω ≼ 𝑎)
193		sdomdomtr 7978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194	190, 192, 193	syl2an 493	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
195	194	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196	184, 195	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
197	126	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
198		breq1 4586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎))
199	198	rspccv 3279	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (suc 𝑀 ∈ 𝑎 → suc 𝑀 ≺ 𝑎))
200	197, 141, 199	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎)
201		omelon 8426	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
202		ontri1 5674	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
203	201, 143, 202	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
204		simplr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
205	13, 204	sylbi 206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
206	205	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
207		sseq2 3590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
208		xpeq12 5058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
209	208	anidms 675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
210		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀)
211	209, 210	breq12d 4596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212	207, 211	imbi12d 333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
213	212	rspccv 3279	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (suc 𝑀 ∈ 𝑎 → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
214	206, 141, 213	sylc 63	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
215	203, 214	sylbird 249	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
216		ensdomtr 7981	. . . . . . . . . . . . . . . . . 18 ⊢ (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
217	216	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑀 ≺ 𝑎 → ((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
218	200, 215, 217	sylsyld 59	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
219	196, 218	pm2.61d 169	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
220		domsdomtr 7980	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
221	183, 219, 220	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
222		ensdomtr 7981	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎)
223	88, 221, 222	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎)
224		ordelon 5664	. . . . . . . . . . . . . . 15 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On)
225	76, 79, 224	sylancr 694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On)
226		onenon 8658	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ On → 𝑎 ∈ dom card)
227	111, 226	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
228		cardsdomel 8683	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
229	225, 227, 228	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
230	223, 229	mpbid 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎))
231		eleq2 2677	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑎) = 𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
232	129, 231	sylbir 224	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
233	17, 197, 232	syl2an2r 872	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
234	230, 233	mpbid 221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎)
235	234	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎)
236		fnfvrnss 6297	. . . . . . . . . . 11 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎)
237		ssdomg 7887	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎))
238	14, 236, 237	mpsyl 66	. . . . . . . . . 10 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎)
239	45, 235, 238	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎)
240		endomtr 7900	. . . . . . . . 9 ⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
241	43, 239, 240	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
242	13, 241	sylbir 224	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
243		df1o2 7459	. . . . . . . . . . . 12 ⊢ 1𝑜 = {∅}
244		1onn 7606	. . . . . . . . . . . 12 ⊢ 1𝑜 ∈ ω
245	243, 244	eqeltrri 2685	. . . . . . . . . . 11 ⊢ {∅} ∈ ω
246		nnsdom 8434	. . . . . . . . . . 11 ⊢ ({∅} ∈ ω → {∅} ≺ ω)
247		sdomdom 7869	. . . . . . . . . . 11 ⊢ ({∅} ≺ ω → {∅} ≼ ω)
248	245, 246, 247	mp2b 10	. . . . . . . . . 10 ⊢ {∅} ≼ ω
249		domtr 7895	. . . . . . . . . 10 ⊢ (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
250	248, 192, 249	sylancr 694	. . . . . . . . 9 ⊢ (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
251		0ex 4718	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
252	14, 251	xpsnen 7929	. . . . . . . . . . 11 ⊢ (𝑎 × {∅}) ≈ 𝑎
253	252	ensymi 7892	. . . . . . . . . 10 ⊢ 𝑎 ≈ (𝑎 × {∅})
254	14	xpdom2 7940	. . . . . . . . . 10 ⊢ ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
255		endomtr 7900	. . . . . . . . . 10 ⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256	253, 254, 255	sylancr 694	. . . . . . . . 9 ⊢ ({∅} ≼ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
257	250, 256	syl 17	. . . . . . . 8 ⊢ (ω ⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
258	257	ad2antrl 760	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
259		sbth 7965	. . . . . . 7 ⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
260	242, 258, 259	syl2anc 691	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
261	260	expr 641	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
262		simplr 788	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
263		simpll 786	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
264		simprr 792	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
265		rexnal 2978	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
266		onelss 5683	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎))
267		ssdomg 7887	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎))
268	266, 267	syld 46	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎))
269		bren2 7872	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎))
270	269	simplbi2 653	. . . . . . . . . . . 12 ⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))
271	268, 270	syl6 34	. . . . . . . . . . 11 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)))
272	271	reximdvai 2998	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
273	265, 272	syl5bir 232	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
274	263, 264, 273	sylc 63	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)
275		r19.29 3054	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
276	262, 274, 275	syl2anc 691	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
277		simprl 790	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
278		onelon 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On)
279		ensym 7891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚)
280		domentr 7901	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚)
281	192, 279, 280	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚)
282		domnsym 7971	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
283		nnsdom 8434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ω → 𝑚 ≺ ω)
284	282, 283	nsyl 134	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
285		ontri1 5674	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
286	201, 285	mpan 702	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
287	284, 286	syl5ibr 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
288	278, 281, 287	syl2im 39	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚))
289	288	expd 451	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)))
290	289	impcom 445	. . . . . . . . . . . . . 14 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))
291	290	imim1d 80	. . . . . . . . . . . . 13 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
292	291	imp32 448	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
293		entr 7894	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
294	293	ancoms 468	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
295		xpen 8008	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
296	295	anidms 675	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
297		entr 7894	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
298	296, 297	sylan 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
299	279, 294, 298	syl2an2r 872	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
300	299	ex 449	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
301	300	ad2antll 761	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
302	292, 301	mpd 15	. . . . . . . . . . 11 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
303	302	ex 449	. . . . . . . . . 10 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304	303	expr 641	. . . . . . . . 9 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
305	304	rexlimdv 3012	. . . . . . . 8 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
306	277, 263, 305	syl2anc 691	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
307	276, 306	mpd 15	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
308	307	expr 641	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
309	261, 308	pm2.61d 169	. . . 4 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
310	309	exp31 628	. . 3 ⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
311	6, 12, 310	tfis3 6949	. 2 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
312	311	imp 444	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131   class class class wbr 4583  {copab 4642   E cep 4947   Se wse 4995   We wwe 4996   × cxp 5036  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  ωcom 6957  1^st c1st 7057  2^nd c2nd 7058  1_𝑜c1o 7440   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841  OrdIsocoi 8297  cardccrd 8644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-oi 8298  df-card 8648

This theorem is referenced by:  infxpen  8720