Theorem infxpenlem 9778

Description: Lemma for infxpen 9779. (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 3948	. . . 4 ⊢ (𝑎 = 𝑚 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝑚))
2		xpeq12 5615	. . . . . 6 ⊢ ((𝑎 = 𝑚 ∧ 𝑎 = 𝑚) → (𝑎 × 𝑎) = (𝑚 × 𝑚))
3	2	anidms 567	. . . . 5 ⊢ (𝑎 = 𝑚 → (𝑎 × 𝑎) = (𝑚 × 𝑚))
4		id 22	. . . . 5 ⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚)
5	3, 4	breq12d 5088	. . . 4 ⊢ (𝑎 = 𝑚 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝑚 × 𝑚) ≈ 𝑚))
6	1, 5	imbi12d 345	. . 3 ⊢ (𝑎 = 𝑚 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)))
7		sseq2 3948	. . . 4 ⊢ (𝑎 = 𝐴 → (ω ⊆ 𝑎 ↔ ω ⊆ 𝐴))
8		xpeq12 5615	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑎 × 𝑎) = (𝐴 × 𝐴))
9	8	anidms 567	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑎) = (𝐴 × 𝐴))
10		id 22	. . . . 5 ⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴)
11	9, 10	breq12d 5088	. . . 4 ⊢ (𝑎 = 𝐴 → ((𝑎 × 𝑎) ≈ 𝑎 ↔ (𝐴 × 𝐴) ≈ 𝐴))
12	7, 11	imbi12d 345	. . 3 ⊢ (𝑎 = 𝐴 → ((ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎) ↔ (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴)))
13		infxpen.2	. . . . . . . 8 ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
14		vex 3437	. . . . . . . . . . . . 13 ⊢ 𝑎 ∈ V
15	14, 14	xpex 7612	. . . . . . . . . . . 12 ⊢ (𝑎 × 𝑎) ∈ V
16		simpll 764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
17	13, 16	sylbi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑎 ∈ On)
18		onss 7643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑎 ⊆ On)
20		xpss12 5605	. . . . . . . . . . . . . . . 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 9777	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
25	24	simpli 484	. . . . . . . . . . . . . . 15 ⊢ 𝑅 We (On × On)
26		wess 5577	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × 𝑎) ⊆ (On × On) → (𝑅 We (On × On) → 𝑅 We (𝑎 × 𝑎)))
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 We (𝑎 × 𝑎))
28		weinxp 5672	. . . . . . . . . . . . . 14 ⊢ (𝑅 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
29	27, 28	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
30		infxpen.1	. . . . . . . . . . . . . 14 ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
31		weeq1 5578	. . . . . . . . . . . . . 14 ⊢ (𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) → (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎)))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑄 We (𝑎 × 𝑎) ↔ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) We (𝑎 × 𝑎))
33	29, 32	sylibr 233	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 We (𝑎 × 𝑎))
34		infxpen.4	. . . . . . . . . . . . 13 ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))
35	34	oiiso 9305	. . . . . . . . . . . 12 ⊢ (((𝑎 × 𝑎) ∈ V ∧ 𝑄 We (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
36	15, 33, 35	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
37		isof1o 7203	. . . . . . . . . . 11 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → 𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎))
38		f1ocnv 6737	. . . . . . . . . . 11 ⊢ (𝐽:dom 𝐽–1-1-onto→(𝑎 × 𝑎) → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽)
39		f1of1 6724	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
41		f1f1orn 6736	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽)
42	15	f1oen 8770	. . . . . . . . . 10 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→ran ◡𝐽 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 × 𝑎) ≈ ran ◡𝐽)
44		f1ofn 6726	. . . . . . . . . . 11 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽 Fn (𝑎 × 𝑎))
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ◡𝐽 Fn (𝑎 × 𝑎))
46	36	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)))
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽)
48		cnvimass 5992	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡𝑄 “ {𝑤}) ⊆ dom 𝑄
49		inss2 4164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
50	30, 49	eqsstri 3956	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎))
51		dmss 5814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ⊆ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) → dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom 𝑄 ⊆ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎))
53		dmxpid 5842	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom ((𝑎 × 𝑎) × (𝑎 × 𝑎)) = (𝑎 × 𝑎)
54	52, 53	sseqtri 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝑄 ⊆ (𝑎 × 𝑎)
55	48, 54	sstri 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)
56		f1ores 6739	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐽:(𝑎 × 𝑎)–1-1→dom 𝐽 ∧ (◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
57	47, 55, 56	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → (◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})))
58	15, 15	xpex 7612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 × 𝑎) × (𝑎 × 𝑎)) ∈ V
59	58	inex2 5243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) ∈ V
60	30, 59	eqeltri 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑄 ∈ V
61	60	cnvex 7781	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡𝑄 ∈ V
62	61	imaex 7772	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑄 “ {𝑤}) ∈ V
63	62	f1oen 8770	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝐽 ↾ (◡𝑄 “ {𝑤})):(◡𝑄 “ {𝑤})–1-1-onto→(◡𝐽 “ (◡𝑄 “ {𝑤})) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
64	46, 57, 63	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽 “ (◡𝑄 “ {𝑤})))
65		sseqin2 4150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑄 “ {𝑤}) ⊆ (𝑎 × 𝑎) ↔ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤}))
66	55, 65	mpbi 229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤})) = (◡𝑄 “ {𝑤})
67	66	imaeq2i 5970	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽 “ (◡𝑄 “ {𝑤}))
68		isocnv 7210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 Isom E , 𝑄 (dom 𝐽, (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽))
70		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑤 ∈ (𝑎 × 𝑎))
71		isoini 7218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝐽 Isom 𝑄, E ((𝑎 × 𝑎), dom 𝐽) ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
72	69, 70, 71	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})))
73		fvex 6796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝐽‘𝑤) ∈ V
74	73	epini 6007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ E “ {(◡𝐽‘𝑤)}) = (◡𝐽‘𝑤)
75	74	ineq2i 4144	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (dom 𝐽 ∩ (◡𝐽‘𝑤))
76	34	oicl 9297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐽
77		f1of 6725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐽:(𝑎 × 𝑎)–1-1-onto→dom 𝐽 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
78	36, 37, 38, 77	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ◡𝐽:(𝑎 × 𝑎)⟶dom 𝐽)
79	78	ffvelrnda 6970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ dom 𝐽)
80		ordelss 6286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
81	76, 79, 80	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ⊆ dom 𝐽)
82		sseqin2 4150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐽‘𝑤) ⊆ dom 𝐽 ↔ (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
83	81, 82	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡𝐽‘𝑤)) = (◡𝐽‘𝑤))
84	75, 83	eqtrid 2791	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (dom 𝐽 ∩ (◡ E “ {(◡𝐽‘𝑤)})) = (◡𝐽‘𝑤))
85	72, 84	eqtrd 2779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ ((𝑎 × 𝑎) ∩ (◡𝑄 “ {𝑤}))) = (◡𝐽‘𝑤))
86	67, 85	eqtr3id 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽 “ (◡𝑄 “ {𝑤})) = (◡𝐽‘𝑤))
87	64, 86	breqtrd 5101	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≈ (◡𝐽‘𝑤))
88	87	ensymd 8800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}))
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))
90		fvex 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1st ‘𝑤) ∈ V
91		fvex 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2nd ‘𝑤) ∈ V
92	90, 91	unex 7605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ V
93	89, 92	eqeltri 2836	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ V
94	93	sucex 7665	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑀 ∈ V
95	94, 94	xpex 7612	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑀 × suc 𝑀) ∈ V
96		xpss 5606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 × 𝑎) ⊆ (V × V)
97		simp3 1137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (◡𝑄 “ {𝑤}))
98		vex 3437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
99	98	eliniseg 6005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ V → (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤))
100	99	elv 3439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (◡𝑄 “ {𝑤}) ↔ 𝑧𝑄𝑤)
101	97, 100	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧𝑄𝑤)
102	30	breqi 5081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧𝑄𝑤 ↔ 𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤)
103		brin 5127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧(𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
104	102, 103	bitri 274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑄𝑤 ↔ (𝑧𝑅𝑤 ∧ 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤))
105	104	simprbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤)
106		brxp 5637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 ↔ (𝑧 ∈ (𝑎 × 𝑎) ∧ 𝑤 ∈ (𝑎 × 𝑎)))
107	106	simplbi 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧((𝑎 × 𝑎) × (𝑎 × 𝑎))𝑤 → 𝑧 ∈ (𝑎 × 𝑎))
108	101, 105, 107	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (𝑎 × 𝑎))
109	96, 108	sselid 3920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (V × V))
110	17	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ On)
111	110	3adant3 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑎 ∈ On)
112		xp1st 7872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (1st ‘𝑧) ∈ 𝑎)
113		onelon 6295	. . . . . . . . . . . . . . . . . . . . . 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 6280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ On → Ord 𝑎)
117		elxp7 7875	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝑎 × 𝑎) ↔ (𝑤 ∈ (V × V) ∧ ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎)))
118	117	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (𝑎 × 𝑎) → ((1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎))
119		ordunel 7683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝑎 ∧ (1st ‘𝑤) ∈ 𝑎 ∧ (2nd ‘𝑤) ∈ 𝑎) → ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∈ 𝑎)
120	119	3expib 1121	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑀 ∈ 𝑎)
124		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
125	13, 124	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
126		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
127	13, 126	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ω ⊆ 𝑎)
128		iscard 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 ↔ (𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))
129		cardlim 9739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎))
130		sseq2 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ (card‘𝑎) ↔ ω ⊆ 𝑎))
131		limeq 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((card‘𝑎) = 𝑎 → (Lim (card‘𝑎) ↔ Lim 𝑎))
132	130, 131	bibi12d 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((card‘𝑎) = 𝑎 → ((ω ⊆ (card‘𝑎) ↔ Lim (card‘𝑎)) ↔ (ω ⊆ 𝑎 ↔ Lim 𝑎)))
133	129, 132	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘𝑎) = 𝑎 → (ω ⊆ 𝑎 ↔ Lim 𝑎))
134	128, 133	sylbir 234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → (ω ⊆ 𝑎 ↔ Lim 𝑎))
135	134	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) ∧ ω ⊆ 𝑎) → Lim 𝑎)
136	17, 125, 127, 135	syl21anc 835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Lim 𝑎)
137	136	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → Lim 𝑎)
138		limsuc 7705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim 𝑎 → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑀 ∈ 𝑎 ↔ suc 𝑀 ∈ 𝑎))
140	123, 139	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ 𝑎)
141		onelon 6295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ On ∧ suc 𝑀 ∈ 𝑎) → suc 𝑀 ∈ On)
142	17, 140, 141	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ∈ On)
143	142	3adant3 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → suc 𝑀 ∈ On)
144		ssun1 4107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
146	104	simplbi 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑄𝑤 → 𝑧𝑅𝑤)
147		df-br 5076	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧𝑅𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑅)
148	23	eleq2i 2831	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑧, 𝑤⟩ ∈ 𝑅 ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))})
149		opabidw 5438	. . . . . . . . . . . . . . . . . . . . . . . . . 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 497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧𝑅𝑤 → (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))
152		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
153	152	orim2i 908	. . . . . . . . . . . . . . . . . . . . . . . 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 6796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1st ‘𝑧) ∈ V
156		fvex 6796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘𝑧) ∈ V
157	155, 156	unex 7605	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ V
158	157	elsuc 6339	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ↔ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤))))
159	154, 158	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
160		suceq 6335	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) → suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤)))
161	89, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑀 = suc ((1st ‘𝑤) ∪ (2nd ‘𝑤))
162	159, 161	eleqtrrdi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧𝑅𝑤 → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
163	101, 146, 162	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)
164		ontr2 6317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (1st ‘𝑧) ∈ suc 𝑀))
165	164	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1st ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (1st ‘𝑧) ∈ suc 𝑀)
166	115, 143, 145, 163, 165	syl22anc 836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (1st ‘𝑧) ∈ suc 𝑀)
167		xp2nd 7873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝑎 × 𝑎) → (2nd ‘𝑧) ∈ 𝑎)
168		onelon 6295	. . . . . . . . . . . . . . . . . . . . . 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 4108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
173		ontr2 6317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) → (((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀) → (2nd ‘𝑧) ∈ suc 𝑀))
174	173	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2nd ‘𝑧) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd ‘𝑧) ⊆ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∧ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ suc 𝑀)) → (2nd ‘𝑧) ∈ suc 𝑀)
175	170, 143, 172, 163, 174	syl22anc 836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → (2nd ‘𝑧) ∈ suc 𝑀)
176		elxp7 7875	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (suc 𝑀 × suc 𝑀) ↔ (𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)))
177	176	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (V × V) ∧ ((1st ‘𝑧) ∈ suc 𝑀 ∧ (2nd ‘𝑧) ∈ suc 𝑀)) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
178	109, 166, 175, 177	syl12anc 834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎) ∧ 𝑧 ∈ (◡𝑄 “ {𝑤})) → 𝑧 ∈ (suc 𝑀 × suc 𝑀))
179	178	3expia 1120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (𝑧 ∈ (◡𝑄 “ {𝑤}) → 𝑧 ∈ (suc 𝑀 × suc 𝑀)))
180	179	ssrdv 3928	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀))
181		ssdomg 8795	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝑀 × suc 𝑀) ∈ V → ((◡𝑄 “ {𝑤}) ⊆ (suc 𝑀 × suc 𝑀) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀)))
182	95, 180, 181	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀))
183	127	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ω ⊆ 𝑎)
184		nnfi 8959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ ω → suc 𝑀 ∈ Fin)
185		xpfi 9094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) → (suc 𝑀 × suc 𝑀) ∈ Fin)
186	185	anidms 567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ∈ Fin)
187		isfinite 9419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑀 × suc 𝑀) ∈ Fin ↔ (suc 𝑀 × suc 𝑀) ≺ ω)
188	186, 187	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑀 ∈ Fin → (suc 𝑀 × suc 𝑀) ≺ ω)
189	184, 188	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ ω)
190		ssdomg 8795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (ω ⊆ 𝑎 → ω ≼ 𝑎))
191	190	elv 3439	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ⊆ 𝑎 → ω ≼ 𝑎)
192		sdomdomtr 8906	. . . . . . . . . . . . . . . . . . 19 ⊢ (((suc 𝑀 × suc 𝑀) ≺ ω ∧ ω ≼ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
193	189, 191, 192	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑀 ∈ ω ∧ ω ⊆ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
194	193	expcom 414	. . . . . . . . . . . . . . . . 17 ⊢ (ω ⊆ 𝑎 → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
195	183, 194	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≺ 𝑎))
196		breq1 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = suc 𝑀 → (𝑚 ≺ 𝑎 ↔ suc 𝑀 ≺ 𝑎))
197	125	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
198	196, 197, 140	rspcdva 3563	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → suc 𝑀 ≺ 𝑎)
199		omelon 9413	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
200		ontri1 6304	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ suc 𝑀 ∈ On) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
201	199, 142, 200	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 ↔ ¬ suc 𝑀 ∈ ω))
202		sseq2 3948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → (ω ⊆ 𝑚 ↔ ω ⊆ suc 𝑀))
203		xpeq12 5615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = suc 𝑀 ∧ 𝑚 = suc 𝑀) → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
204	203	anidms 567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → (𝑚 × 𝑚) = (suc 𝑀 × suc 𝑀))
205		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = suc 𝑀 → 𝑚 = suc 𝑀)
206	204, 205	breq12d 5088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = suc 𝑀 → ((𝑚 × 𝑚) ≈ 𝑚 ↔ (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
207	202, 206	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = suc 𝑀 → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ↔ (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀)))
208		simplr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
209	13, 208	sylbi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
210	209	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
211	207, 210, 140	rspcdva 3563	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (ω ⊆ suc 𝑀 → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
212	201, 211	sylbird 259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (¬ suc 𝑀 ∈ ω → (suc 𝑀 × suc 𝑀) ≈ suc 𝑀))
213		ensdomtr 8909	. . . . . . . . . . . . . . . . . 18 ⊢ (((suc 𝑀 × suc 𝑀) ≈ suc 𝑀 ∧ suc 𝑀 ≺ 𝑎) → (suc 𝑀 × suc 𝑀) ≺ 𝑎)
214	213	expcom 414	. . . . . . . . . . . . . . . . 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 8908	. . . . . . . . . . . . . . 15 ⊢ (((◡𝑄 “ {𝑤}) ≼ (suc 𝑀 × suc 𝑀) ∧ (suc 𝑀 × suc 𝑀) ≺ 𝑎) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
218	182, 216, 217	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝑄 “ {𝑤}) ≺ 𝑎)
219		ensdomtr 8909	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ≈ (◡𝑄 “ {𝑤}) ∧ (◡𝑄 “ {𝑤}) ≺ 𝑎) → (◡𝐽‘𝑤) ≺ 𝑎)
220	88, 218, 219	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ≺ 𝑎)
221		ordelon 6294	. . . . . . . . . . . . . . 15 ⊢ ((Ord dom 𝐽 ∧ (◡𝐽‘𝑤) ∈ dom 𝐽) → (◡𝐽‘𝑤) ∈ On)
222	76, 79, 221	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ On)
223		onenon 9716	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ On → 𝑎 ∈ dom card)
224	110, 223	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → 𝑎 ∈ dom card)
225		cardsdomel 9741	. . . . . . . . . . . . . 14 ⊢ (((◡𝐽‘𝑤) ∈ On ∧ 𝑎 ∈ dom card) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
226	222, 224, 225	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ≺ 𝑎 ↔ (◡𝐽‘𝑤) ∈ (card‘𝑎)))
227	220, 226	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ (card‘𝑎))
228		eleq2 2828	. . . . . . . . . . . . . 14 ⊢ ((card‘𝑎) = 𝑎 → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
229	128, 228	sylbir 234	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
230	17, 197, 229	syl2an2r 682	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → ((◡𝐽‘𝑤) ∈ (card‘𝑎) ↔ (◡𝐽‘𝑤) ∈ 𝑎))
231	227, 230	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑎 × 𝑎)) → (◡𝐽‘𝑤) ∈ 𝑎)
232	231	ralrimiva 3104	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎)
233		fnfvrnss 7003	. . . . . . . . . . 11 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ⊆ 𝑎)
234		ssdomg 8795	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V → (ran ◡𝐽 ⊆ 𝑎 → ran ◡𝐽 ≼ 𝑎))
235	14, 233, 234	mpsyl 68	. . . . . . . . . 10 ⊢ ((◡𝐽 Fn (𝑎 × 𝑎) ∧ ∀𝑤 ∈ (𝑎 × 𝑎)(◡𝐽‘𝑤) ∈ 𝑎) → ran ◡𝐽 ≼ 𝑎)
236	45, 232, 235	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ran ◡𝐽 ≼ 𝑎)
237		endomtr 8807	. . . . . . . . 9 ⊢ (((𝑎 × 𝑎) ≈ ran ◡𝐽 ∧ ran ◡𝐽 ≼ 𝑎) → (𝑎 × 𝑎) ≼ 𝑎)
238	43, 236, 237	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑎 × 𝑎) ≼ 𝑎)
239	13, 238	sylbir 234	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≼ 𝑎)
240		df1o2 8313	. . . . . . . . . . . 12 ⊢ 1o = {∅}
241		1onn 8479	. . . . . . . . . . . 12 ⊢ 1o ∈ ω
242	240, 241	eqeltrri 2837	. . . . . . . . . . 11 ⊢ {∅} ∈ ω
243		nnsdom 9421	. . . . . . . . . . 11 ⊢ ({∅} ∈ ω → {∅} ≺ ω)
244		sdomdom 8777	. . . . . . . . . . 11 ⊢ ({∅} ≺ ω → {∅} ≼ ω)
245	242, 243, 244	mp2b 10	. . . . . . . . . 10 ⊢ {∅} ≼ ω
246		domtr 8802	. . . . . . . . . 10 ⊢ (({∅} ≼ ω ∧ ω ≼ 𝑎) → {∅} ≼ 𝑎)
247	245, 191, 246	sylancr 587	. . . . . . . . 9 ⊢ (ω ⊆ 𝑎 → {∅} ≼ 𝑎)
248		0ex 5232	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
249	14, 248	xpsnen 8851	. . . . . . . . . . 11 ⊢ (𝑎 × {∅}) ≈ 𝑎
250	249	ensymi 8799	. . . . . . . . . 10 ⊢ 𝑎 ≈ (𝑎 × {∅})
251	14	xpdom2 8863	. . . . . . . . . 10 ⊢ ({∅} ≼ 𝑎 → (𝑎 × {∅}) ≼ (𝑎 × 𝑎))
252		endomtr 8807	. . . . . . . . . 10 ⊢ ((𝑎 ≈ (𝑎 × {∅}) ∧ (𝑎 × {∅}) ≼ (𝑎 × 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
253	250, 251, 252	sylancr 587	. . . . . . . . 9 ⊢ ({∅} ≼ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
254	247, 253	syl 17	. . . . . . . 8 ⊢ (ω ⊆ 𝑎 → 𝑎 ≼ (𝑎 × 𝑎))
255	254	ad2antrl 725	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ≼ (𝑎 × 𝑎))
256		sbth 8889	. . . . . . 7 ⊢ (((𝑎 × 𝑎) ≼ 𝑎 ∧ 𝑎 ≼ (𝑎 × 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
257	239, 255, 256	syl2anc 584	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
258	257	expr 457	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
259		simplr 766	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚))
260		simpll 764	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → 𝑎 ∈ On)
261		simprr 770	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
262		rexnal 3170	. . . . . . . . . 10 ⊢ (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 ↔ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)
263		onelss 6312	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ⊆ 𝑎))
264		ssdomg 8795	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ On → (𝑚 ⊆ 𝑎 → 𝑚 ≼ 𝑎))
265	263, 264	syld 47	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → 𝑚 ≼ 𝑎))
266		bren2 8780	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 ↔ (𝑚 ≼ 𝑎 ∧ ¬ 𝑚 ≺ 𝑎))
267	266	simplbi2 501	. . . . . . . . . . . 12 ⊢ (𝑚 ≼ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎))
268	265, 267	syl6 35	. . . . . . . . . . 11 ⊢ (𝑎 ∈ On → (𝑚 ∈ 𝑎 → (¬ 𝑚 ≺ 𝑎 → 𝑚 ≈ 𝑎)))
269	268	reximdvai 3201	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (∃𝑚 ∈ 𝑎 ¬ 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
270	262, 269	syl5bir 242	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎))
271	260, 261, 270	sylc 65	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎)
272		r19.29 3185	. . . . . . . 8 ⊢ ((∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ ∃𝑚 ∈ 𝑎 𝑚 ≈ 𝑎) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
273	259, 271, 272	syl2anc 584	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎))
274		simprl 768	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → ω ⊆ 𝑎)
275		onelon 6295	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → 𝑚 ∈ On)
276		ensym 8798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ≈ 𝑎 → 𝑎 ≈ 𝑚)
277		domentr 8808	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ≼ 𝑎 ∧ 𝑎 ≈ 𝑚) → ω ≼ 𝑚)
278	191, 276, 277	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ≼ 𝑚)
279		domnsym 8895	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ≺ ω)
280		nnsdom 9421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ω → 𝑚 ≺ ω)
281	279, 280	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≼ 𝑚 → ¬ 𝑚 ∈ ω)
282		ontri1 6304	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ω ∈ On ∧ 𝑚 ∈ On) → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
283	199, 282	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ On → (ω ⊆ 𝑚 ↔ ¬ 𝑚 ∈ ω))
284	281, 283	syl5ibr 245	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ On → (ω ≼ 𝑚 → ω ⊆ 𝑚))
285	275, 278, 284	syl2im 40	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → ((ω ⊆ 𝑎 ∧ 𝑚 ≈ 𝑎) → ω ⊆ 𝑚))
286	285	expd 416	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ On ∧ 𝑚 ∈ 𝑎) → (ω ⊆ 𝑎 → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚)))
287	286	impcom 408	. . . . . . . . . . . . . 14 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (𝑚 ≈ 𝑎 → ω ⊆ 𝑚))
288	287	imim1d 82	. . . . . . . . . . . . 13 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 ≈ 𝑎 → (𝑚 × 𝑚) ≈ 𝑚)))
289	288	imp32 419	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑚 × 𝑚) ≈ 𝑚)
290		entr 8801	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 × 𝑚) ≈ 𝑚 ∧ 𝑚 ≈ 𝑎) → (𝑚 × 𝑚) ≈ 𝑎)
291	290	ancoms 459	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑚 × 𝑚) ≈ 𝑎)
292		xpen 8936	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≈ 𝑚 ∧ 𝑎 ≈ 𝑚) → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
293	292	anidms 567	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ≈ 𝑚 → (𝑎 × 𝑎) ≈ (𝑚 × 𝑚))
294		entr 8801	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑎) ≈ (𝑚 × 𝑚) ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
295	293, 294	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≈ 𝑚 ∧ (𝑚 × 𝑚) ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
296	276, 291, 295	syl2an2r 682	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ≈ 𝑎 ∧ (𝑚 × 𝑚) ≈ 𝑚) → (𝑎 × 𝑎) ≈ 𝑎)
297	296	ex 413	. . . . . . . . . . . . 13 ⊢ (𝑚 ≈ 𝑎 → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
298	297	ad2antll 726	. . . . . . . . . . . 12 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → ((𝑚 × 𝑚) ≈ 𝑚 → (𝑎 × 𝑎) ≈ 𝑎))
299	289, 298	mpd 15	. . . . . . . . . . 11 ⊢ (((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) ∧ ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
300	299	ex 413	. . . . . . . . . 10 ⊢ ((ω ⊆ 𝑎 ∧ (𝑎 ∈ On ∧ 𝑚 ∈ 𝑎)) → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
301	300	expr 457	. . . . . . . . 9 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (𝑚 ∈ 𝑎 → (((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)))
302	301	rexlimdv 3213	. . . . . . . 8 ⊢ ((ω ⊆ 𝑎 ∧ 𝑎 ∈ On) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
303	274, 260, 302	syl2anc 584	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (∃𝑚 ∈ 𝑎 ((ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) ∧ 𝑚 ≈ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎))
304	273, 303	mpd 15	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) → (𝑎 × 𝑎) ≈ 𝑎)
305	304	expr 457	. . . . 5 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (¬ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎))
306	258, 305	pm2.61d 179	. . . 4 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ ω ⊆ 𝑎) → (𝑎 × 𝑎) ≈ 𝑎)
307	306	exp31 420	. . 3 ⊢ (𝑎 ∈ On → (∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚) → (ω ⊆ 𝑎 → (𝑎 × 𝑎) ≈ 𝑎)))
308	6, 12, 307	tfis3 7713	. 2 ⊢ (𝐴 ∈ On → (ω ⊆ 𝐴 → (𝐴 × 𝐴) ≈ 𝐴))
309	308	imp 407	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ∀wral 3065  ∃wrex 3066  Vcvv 3433   ∪ cun 3886   ∩ cin 3887   ⊆ wss 3888  ∅c0 4257  {csn 4562  ⟨cop 4568   class class class wbr 5075  {copab 5137   E cep 5495   Se wse 5543   We wwe 5544   × cxp 5588  ^◡ccnv 5589  dom cdm 5590  ran crn 5591   ↾ cres 5592   “ cima 5593  Ord word 6269  Oncon0 6270  Lim wlim 6271  suc csuc 6272   Fn wfn 6432  ⟶wf 6433  –1-1→wf1 6434  –1-1-onto→wf1o 6436  ‘cfv 6437   Isom wiso 6438  ωcom 7721  1^st c1st 7838  2^nd c2nd 7839  1_oc1o 8299   ≈ cen 8739   ≼ cdom 8740   ≺ csdm 8741  Fincfn 8742  OrdIsocoi 9277  cardccrd 9702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-oi 9278  df-card 9706

This theorem is referenced by:  infxpen  9779