MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infxpenlem Structured version   Visualization version   GIF version
Theorem infxpenlem 10005
Description: Lemma for infxpen 10006. (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
StepHypRef Expression
1 sseq2 4008 . . . 4 (π‘Ž = π‘š β†’ (Ο‰ βŠ† π‘Ž ↔ Ο‰ βŠ† π‘š))
2 xpeq12 5701 . . . . . 6 ((π‘Ž = π‘š ∧ π‘Ž = π‘š) β†’ (π‘Ž Γ— π‘Ž) = (π‘š Γ— π‘š))
32anidms 568 . . . . 5 (π‘Ž = π‘š β†’ (π‘Ž Γ— π‘Ž) = (π‘š Γ— π‘š))
4 id 22 . . . . 5 (π‘Ž = π‘š β†’ π‘Ž = π‘š)
53, 4breq12d 5161 . . . 4 (π‘Ž = π‘š β†’ ((π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž ↔ (π‘š Γ— π‘š) β‰ˆ π‘š))
61, 5imbi12d 345 . . 3 (π‘Ž = π‘š β†’ ((Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž) ↔ (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)))
7 sseq2 4008 . . . 4 (π‘Ž = 𝐴 β†’ (Ο‰ βŠ† π‘Ž ↔ Ο‰ βŠ† 𝐴))
8 xpeq12 5701 . . . . . 6 ((π‘Ž = 𝐴 ∧ π‘Ž = 𝐴) β†’ (π‘Ž Γ— π‘Ž) = (𝐴 Γ— 𝐴))
98anidms 568 . . . . 5 (π‘Ž = 𝐴 β†’ (π‘Ž Γ— π‘Ž) = (𝐴 Γ— 𝐴))
10 id 22 . . . . 5 (π‘Ž = 𝐴 β†’ π‘Ž = 𝐴)
119, 10breq12d 5161 . . . 4 (π‘Ž = 𝐴 β†’ ((π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž ↔ (𝐴 Γ— 𝐴) β‰ˆ 𝐴))
127, 11imbi12d 345 . . 3 (π‘Ž = 𝐴 β†’ ((Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž) ↔ (Ο‰ βŠ† 𝐴 β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴)))
13 infxpen.2 . . . . . . . 8 (πœ‘ ↔ ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)))
14 vex 3479 . . . . . . . . . . . . 13 π‘Ž ∈ V
1514, 14xpex 7737 . . . . . . . . . . . 12 (π‘Ž Γ— π‘Ž) ∈ V
16 simpll 766 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž ∈ On)
1713, 16sylbi 216 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Ž ∈ On)
18 onss 7769 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ On β†’ π‘Ž βŠ† On)
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘Ž βŠ† On)
20 xpss12 5691 . . . . . . . . . . . . . . . 16 ((π‘Ž βŠ† On ∧ π‘Ž βŠ† On) β†’ (π‘Ž Γ— π‘Ž) βŠ† (On Γ— On))
2119, 19, 20syl2anc 585 . . . . . . . . . . . . . . 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 β€˜π‘€)) ∧ 𝑧𝐿𝑀)))}
2422, 23r0weon 10004 . . . . . . . . . . . . . . . 16 (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On))
2524simpli 485 . . . . . . . . . . . . . . 15 𝑅 We (On Γ— On)
26 wess 5663 . . . . . . . . . . . . . . 15 ((π‘Ž Γ— π‘Ž) βŠ† (On Γ— On) β†’ (𝑅 We (On Γ— On) β†’ 𝑅 We (π‘Ž Γ— π‘Ž)))
2721, 25, 26mpisyl 21 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 We (π‘Ž Γ— π‘Ž))
28 weinxp 5759 . . . . . . . . . . . . . 14 (𝑅 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
2927, 28sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
30 infxpen.1 . . . . . . . . . . . . . 14 𝑄 = (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))
31 weeq1 5664 . . . . . . . . . . . . . 14 (𝑄 = (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) β†’ (𝑄 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž)))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 (𝑄 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
3329, 32sylibr 233 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 We (π‘Ž Γ— π‘Ž))
34 infxpen.4 . . . . . . . . . . . . 13 𝐽 = OrdIso(𝑄, (π‘Ž Γ— π‘Ž))
3534oiiso 9529 . . . . . . . . . . . 12 (((π‘Ž Γ— π‘Ž) ∈ V ∧ 𝑄 We (π‘Ž Γ— π‘Ž)) β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
3615, 33, 35sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
37 isof1o 7317 . . . . . . . . . . 11 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ 𝐽:dom 𝐽–1-1-ontoβ†’(π‘Ž Γ— π‘Ž))
38 f1ocnv 6843 . . . . . . . . . . 11 (𝐽:dom 𝐽–1-1-ontoβ†’(π‘Ž Γ— π‘Ž) β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽)
39 f1of1 6830 . . . . . . . . . . 11 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
4036, 37, 38, 394syl 19 . . . . . . . . . 10 (πœ‘ β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
41 f1f1orn 6842 . . . . . . . . . 10 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’ran ◑𝐽)
4215f1oen 8966 . . . . . . . . . 10 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’ran ◑𝐽 β†’ (π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽)
4340, 41, 423syl 18 . . . . . . . . 9 (πœ‘ β†’ (π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽)
44 f1ofn 6832 . . . . . . . . . . 11 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽 Fn (π‘Ž Γ— π‘Ž))
4536, 37, 38, 444syl 19 . . . . . . . . . 10 (πœ‘ β†’ ◑𝐽 Fn (π‘Ž Γ— π‘Ž))
4636adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
4737, 38, 393syl 18 . . . . . . . . . . . . . . . . . 18 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
48 cnvimass 6078 . . . . . . . . . . . . . . . . . . 19 (◑𝑄 β€œ {𝑀}) βŠ† dom 𝑄
49 inss2 4229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
5030, 49eqsstri 4016 . . . . . . . . . . . . . . . . . . . . 21 𝑄 βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
51 dmss 5901 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) β†’ dom 𝑄 βŠ† dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 dom 𝑄 βŠ† dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
53 dmxpid 5928 . . . . . . . . . . . . . . . . . . . 20 dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) = (π‘Ž Γ— π‘Ž)
5452, 53sseqtri 4018 . . . . . . . . . . . . . . . . . . 19 dom 𝑄 βŠ† (π‘Ž Γ— π‘Ž)
5548, 54sstri 3991 . . . . . . . . . . . . . . . . . 18 (◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž)
56 f1ores 6845 . . . . . . . . . . . . . . . . . 18 ((◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽 ∧ (◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
5747, 55, 56sylancl 587 . . . . . . . . . . . . . . . . 17 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
5815, 15xpex 7737 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) ∈ V
5958inex2 5318 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) ∈ V
6030, 59eqeltri 2830 . . . . . . . . . . . . . . . . . . . 20 𝑄 ∈ V
6160cnvex 7913 . . . . . . . . . . . . . . . . . . 19 ◑𝑄 ∈ V
6261imaex 7904 . . . . . . . . . . . . . . . . . 18 (◑𝑄 β€œ {𝑀}) ∈ V
6362f1oen 8966 . . . . . . . . . . . . . . . . 17 ((◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
6446, 57, 633syl 18 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
65 sseqin2 4215 . . . . . . . . . . . . . . . . . . 19 ((◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž) ↔ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀})) = (◑𝑄 β€œ {𝑀}))
6655, 65mpbi 229 . . . . . . . . . . . . . . . . . 18 ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀})) = (◑𝑄 β€œ {𝑀})
6766imaeq2i 6056 . . . . . . . . . . . . . . . . 17 (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (◑𝐽 β€œ (◑𝑄 β€œ {𝑀}))
68 isocnv 7324 . . . . . . . . . . . . . . . . . . . 20 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽))
6946, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽))
70 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝑀 ∈ (π‘Ž Γ— π‘Ž))
71 isoini 7332 . . . . . . . . . . . . . . . . . . 19 ((◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽) ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})))
7269, 70, 71syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})))
73 fvex 6902 . . . . . . . . . . . . . . . . . . . . 21 (β—‘π½β€˜π‘€) ∈ V
7473epini 6093 . . . . . . . . . . . . . . . . . . . 20 (β—‘ E β€œ {(β—‘π½β€˜π‘€)}) = (β—‘π½β€˜π‘€)
7574ineq2i 4209 . . . . . . . . . . . . . . . . . . 19 (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})) = (dom 𝐽 ∩ (β—‘π½β€˜π‘€))
7634oicl 9521 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐽
77 f1of 6831 . . . . . . . . . . . . . . . . . . . . . . 23 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)⟢dom 𝐽)
7836, 37, 38, 774syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)⟢dom 𝐽)
7978ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ dom 𝐽)
80 ordelss 6378 . . . . . . . . . . . . . . . . . . . . 21 ((Ord dom 𝐽 ∧ (β—‘π½β€˜π‘€) ∈ dom 𝐽) β†’ (β—‘π½β€˜π‘€) βŠ† dom 𝐽)
8176, 79, 80sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) βŠ† dom 𝐽)
82 sseqin2 4215 . . . . . . . . . . . . . . . . . . . 20 ((β—‘π½β€˜π‘€) βŠ† dom 𝐽 ↔ (dom 𝐽 ∩ (β—‘π½β€˜π‘€)) = (β—‘π½β€˜π‘€))
8381, 82sylib 217 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (dom 𝐽 ∩ (β—‘π½β€˜π‘€)) = (β—‘π½β€˜π‘€))
8475, 83eqtrid 2785 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})) = (β—‘π½β€˜π‘€))
8572, 84eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (β—‘π½β€˜π‘€))
8667, 85eqtr3id 2787 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})) = (β—‘π½β€˜π‘€))
8764, 86breqtrd 5174 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (β—‘π½β€˜π‘€))
8887ensymd 8998 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) β‰ˆ (◑𝑄 β€œ {𝑀}))
89 infxpen.3 . . . . . . . . . . . . . . . . . . 19 𝑀 = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))
90 fvex 6902 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜π‘€) ∈ V
91 fvex 6902 . . . . . . . . . . . . . . . . . . . 20 (2nd β€˜π‘€) ∈ V
9290, 91unex 7730 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ V
9389, 92eqeltri 2830 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
9493sucex 7791 . . . . . . . . . . . . . . . . 17 suc 𝑀 ∈ V
9594, 94xpex 7737 . . . . . . . . . . . . . . . 16 (suc 𝑀 Γ— suc 𝑀) ∈ V
96 xpss 5692 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž Γ— π‘Ž) βŠ† (V Γ— V)
97 simp3 1139 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (◑𝑄 β€œ {𝑀}))
98 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
9998eliniseg 6091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ V β†’ (𝑧 ∈ (◑𝑄 β€œ {𝑀}) ↔ 𝑧𝑄𝑀))
10099elv 3481 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (◑𝑄 β€œ {𝑀}) ↔ 𝑧𝑄𝑀)
10197, 100sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧𝑄𝑀)
10230breqi 5154 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑄𝑀 ↔ 𝑧(𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))𝑀)
103 brin 5200 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧(𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))𝑀 ↔ (𝑧𝑅𝑀 ∧ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀))
104102, 103bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑄𝑀 ↔ (𝑧𝑅𝑀 ∧ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀))
105104simprbi 498 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑀 β†’ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀)
106 brxp 5724 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀 ↔ (𝑧 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)))
107106simplbi 499 . . . . . . . . . . . . . . . . . . . . 21 (𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀 β†’ 𝑧 ∈ (π‘Ž Γ— π‘Ž))
108101, 105, 1073syl 18 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (π‘Ž Γ— π‘Ž))
10996, 108sselid 3980 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (V Γ— V))
11017adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ π‘Ž ∈ On)
1111103adant3 1133 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ π‘Ž ∈ On)
112 xp1st 8004 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (π‘Ž Γ— π‘Ž) β†’ (1st β€˜π‘§) ∈ π‘Ž)
113 onelon 6387 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ (1st β€˜π‘§) ∈ π‘Ž) β†’ (1st β€˜π‘§) ∈ On)
114112, 113sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ On ∧ 𝑧 ∈ (π‘Ž Γ— π‘Ž)) β†’ (1st β€˜π‘§) ∈ On)
115111, 108, 114syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) ∈ On)
116 eloni 6372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž ∈ On β†’ Ord π‘Ž)
117 elxp7 8007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ (π‘Ž Γ— π‘Ž) ↔ (𝑀 ∈ (V Γ— V) ∧ ((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž)))
118117simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ (π‘Ž Γ— π‘Ž) β†’ ((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž))
119 ordunel 7812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord π‘Ž ∧ (1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž)
1201193expib 1123 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord π‘Ž β†’ (((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž))
121116, 118, 120syl2im 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ On β†’ (𝑀 ∈ (π‘Ž Γ— π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž))
122110, 70, 121sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž)
12389, 122eqeltrid 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝑀 ∈ π‘Ž)
124 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
12513, 124sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
126 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
12713, 126sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ Ο‰ βŠ† π‘Ž)
128 iscard 9967 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((cardβ€˜π‘Ž) = π‘Ž ↔ (π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž))
129 cardlim 9964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Lim (cardβ€˜π‘Ž))
130 sseq2 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Ο‰ βŠ† π‘Ž))
131 limeq 6374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Lim (cardβ€˜π‘Ž) ↔ Lim π‘Ž))
132130, 131bibi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((cardβ€˜π‘Ž) = π‘Ž β†’ ((Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Lim (cardβ€˜π‘Ž)) ↔ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž)))
133129, 132mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž))
134128, 133sylbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) β†’ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž))
135134biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) ∧ Ο‰ βŠ† π‘Ž) β†’ Lim π‘Ž)
13617, 125, 127, 135syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ Lim π‘Ž)
137136adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ Lim π‘Ž)
138 limsuc 7835 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim π‘Ž β†’ (𝑀 ∈ π‘Ž ↔ suc 𝑀 ∈ π‘Ž))
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (𝑀 ∈ π‘Ž ↔ suc 𝑀 ∈ π‘Ž))
140123, 139mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 ∈ π‘Ž)
141 onelon 6387 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ suc 𝑀 ∈ π‘Ž) β†’ suc 𝑀 ∈ On)
14217, 140, 141syl2an2r 684 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 ∈ On)
1431423adant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ suc 𝑀 ∈ On)
144 ssun1 4172 . . . . . . . . . . . . . . . . . . . . 21 (1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§))
145144a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
146104simplbi 499 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑀 β†’ 𝑧𝑅𝑀)
147 df-br 5149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑅𝑀 ↔ βŸ¨π‘§, π‘€βŸ© ∈ 𝑅)
14823eleq2i 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βŸ¨π‘§, π‘€βŸ© ∈ 𝑅 ↔ βŸ¨π‘§, π‘€βŸ© ∈ {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))})
149 opabidw 5524 . . . . . . . . . . . . . . . . . . . . . . . . . 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 β€˜π‘€)) ∧ 𝑧𝐿𝑀))))
150147, 148, 1493bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑅𝑀 ↔ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀))))
151150simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧𝑅𝑀 β†’ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))
152 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀) β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
153152orim2i 910 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)) β†’ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
154151, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑅𝑀 β†’ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
155 fvex 6902 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1st β€˜π‘§) ∈ V
156 fvex 6902 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd β€˜π‘§) ∈ V
157155, 156unex 7730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ V
158157elsuc 6432 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ↔ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))))
159154, 158sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑅𝑀 β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
160 suceq 6428 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) β†’ suc 𝑀 = suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
16189, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑀 = suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))
162159, 161eleqtrrdi 2845 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑅𝑀 β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)
163101, 146, 1623syl 18 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)
164 ontr2 6409 . . . . . . . . . . . . . . . . . . . . 21 (((1st β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) β†’ (((1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀) β†’ (1st β€˜π‘§) ∈ suc 𝑀))
165164imp 408 . . . . . . . . . . . . . . . . . . . 20 ((((1st β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)) β†’ (1st β€˜π‘§) ∈ suc 𝑀)
166115, 143, 145, 163, 165syl22anc 838 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) ∈ suc 𝑀)
167 xp2nd 8005 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (π‘Ž Γ— π‘Ž) β†’ (2nd β€˜π‘§) ∈ π‘Ž)
168 onelon 6387 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ (2nd β€˜π‘§) ∈ π‘Ž) β†’ (2nd β€˜π‘§) ∈ On)
169167, 168sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ On ∧ 𝑧 ∈ (π‘Ž Γ— π‘Ž)) β†’ (2nd β€˜π‘§) ∈ On)
170111, 108, 169syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) ∈ On)
171 ssun2 4173 . . . . . . . . . . . . . . . . . . . . 21 (2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§))
172171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
173 ontr2 6409 . . . . . . . . . . . . . . . . . . . . 21 (((2nd β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) β†’ (((2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀) β†’ (2nd β€˜π‘§) ∈ suc 𝑀))
174173imp 408 . . . . . . . . . . . . . . . . . . . 20 ((((2nd β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)) β†’ (2nd β€˜π‘§) ∈ suc 𝑀)
175170, 143, 172, 163, 174syl22anc 838 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) ∈ suc 𝑀)
176 elxp7 8007 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (suc 𝑀 Γ— suc 𝑀) ↔ (𝑧 ∈ (V Γ— V) ∧ ((1st β€˜π‘§) ∈ suc 𝑀 ∧ (2nd β€˜π‘§) ∈ suc 𝑀)))
177176biimpri 227 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (V Γ— V) ∧ ((1st β€˜π‘§) ∈ suc 𝑀 ∧ (2nd β€˜π‘§) ∈ suc 𝑀)) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀))
178109, 166, 175, 177syl12anc 836 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀))
1791783expia 1122 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (𝑧 ∈ (◑𝑄 β€œ {𝑀}) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀)))
180179ssrdv 3988 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) βŠ† (suc 𝑀 Γ— suc 𝑀))
181 ssdomg 8993 . . . . . . . . . . . . . . . 16 ((suc 𝑀 Γ— suc 𝑀) ∈ V β†’ ((◑𝑄 β€œ {𝑀}) βŠ† (suc 𝑀 Γ— suc 𝑀) β†’ (◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀)))
18295, 180, 181mpsyl 68 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀))
183127adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
184 nnfi 9164 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Ο‰ β†’ suc 𝑀 ∈ Fin)
185 xpfi 9314 . . . . . . . . . . . . . . . . . . . . . 22 ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) β†’ (suc 𝑀 Γ— suc 𝑀) ∈ Fin)
186185anidms 568 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑀 ∈ Fin β†’ (suc 𝑀 Γ— suc 𝑀) ∈ Fin)
187 isfinite 9644 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑀 Γ— suc 𝑀) ∈ Fin ↔ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
188186, 187sylib 217 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Fin β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
189184, 188syl 17 . . . . . . . . . . . . . . . . . . 19 (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
190 ssdomg 8993 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž ∈ V β†’ (Ο‰ βŠ† π‘Ž β†’ Ο‰ β‰Ό π‘Ž))
191190elv 3481 . . . . . . . . . . . . . . . . . . 19 (Ο‰ βŠ† π‘Ž β†’ Ο‰ β‰Ό π‘Ž)
192 sdomdomtr 9107 . . . . . . . . . . . . . . . . . . 19 (((suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰ ∧ Ο‰ β‰Ό π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
193189, 191, 192syl2an 597 . . . . . . . . . . . . . . . . . 18 ((suc 𝑀 ∈ Ο‰ ∧ Ο‰ βŠ† π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
194193expcom 415 . . . . . . . . . . . . . . . . 17 (Ο‰ βŠ† π‘Ž β†’ (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
195183, 194syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
196 breq1 5151 . . . . . . . . . . . . . . . . . 18 (π‘š = suc 𝑀 β†’ (π‘š β‰Ί π‘Ž ↔ suc 𝑀 β‰Ί π‘Ž))
197125adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
198196, 197, 140rspcdva 3614 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 β‰Ί π‘Ž)
199 omelon 9638 . . . . . . . . . . . . . . . . . . 19 Ο‰ ∈ On
200 ontri1 6396 . . . . . . . . . . . . . . . . . . 19 ((Ο‰ ∈ On ∧ suc 𝑀 ∈ On) β†’ (Ο‰ βŠ† suc 𝑀 ↔ Β¬ suc 𝑀 ∈ Ο‰))
201199, 142, 200sylancr 588 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Ο‰ βŠ† suc 𝑀 ↔ Β¬ suc 𝑀 ∈ Ο‰))
202 sseq2 4008 . . . . . . . . . . . . . . . . . . . 20 (π‘š = suc 𝑀 β†’ (Ο‰ βŠ† π‘š ↔ Ο‰ βŠ† suc 𝑀))
203 xpeq12 5701 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š = suc 𝑀 ∧ π‘š = suc 𝑀) β†’ (π‘š Γ— π‘š) = (suc 𝑀 Γ— suc 𝑀))
204203anidms 568 . . . . . . . . . . . . . . . . . . . . 21 (π‘š = suc 𝑀 β†’ (π‘š Γ— π‘š) = (suc 𝑀 Γ— suc 𝑀))
205 id 22 . . . . . . . . . . . . . . . . . . . . 21 (π‘š = suc 𝑀 β†’ π‘š = suc 𝑀)
206204, 205breq12d 5161 . . . . . . . . . . . . . . . . . . . 20 (π‘š = suc 𝑀 β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š ↔ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
207202, 206imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (π‘š = suc 𝑀 β†’ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ↔ (Ο‰ βŠ† suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀)))
208 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
20913, 208sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
210209adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
211207, 210, 140rspcdva 3614 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Ο‰ βŠ† suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
212201, 211sylbird 260 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Β¬ suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
213 ensdomtr 9110 . . . . . . . . . . . . . . . . . 18 (((suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀 ∧ suc 𝑀 β‰Ί π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
214213expcom 415 . . . . . . . . . . . . . . . . 17 (suc 𝑀 β‰Ί π‘Ž β†’ ((suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
215198, 212, 214sylsyld 61 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Β¬ suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
216195, 215pm2.61d 179 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
217 domsdomtr 9109 . . . . . . . . . . . . . . 15 (((◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀) ∧ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž) β†’ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž)
218182, 216, 217syl2anc 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž)
219 ensdomtr 9110 . . . . . . . . . . . . . 14 (((β—‘π½β€˜π‘€) β‰ˆ (◑𝑄 β€œ {𝑀}) ∧ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž) β†’ (β—‘π½β€˜π‘€) β‰Ί π‘Ž)
22088, 218, 219syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) β‰Ί π‘Ž)
221 ordelon 6386 . . . . . . . . . . . . . . 15 ((Ord dom 𝐽 ∧ (β—‘π½β€˜π‘€) ∈ dom 𝐽) β†’ (β—‘π½β€˜π‘€) ∈ On)
22276, 79, 221sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ On)
223 onenon 9941 . . . . . . . . . . . . . . 15 (π‘Ž ∈ On β†’ π‘Ž ∈ dom card)
224110, 223syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ π‘Ž ∈ dom card)
225 cardsdomel 9966 . . . . . . . . . . . . . 14 (((β—‘π½β€˜π‘€) ∈ On ∧ π‘Ž ∈ dom card) β†’ ((β—‘π½β€˜π‘€) β‰Ί π‘Ž ↔ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž)))
226222, 224, 225syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((β—‘π½β€˜π‘€) β‰Ί π‘Ž ↔ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž)))
227220, 226mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž))
228 eleq2 2823 . . . . . . . . . . . . . 14 ((cardβ€˜π‘Ž) = π‘Ž β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
229128, 228sylbir 234 . . . . . . . . . . . . 13 ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
23017, 197, 229syl2an2r 684 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
231227, 230mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ π‘Ž)
232231ralrimiva 3147 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž)
233 fnfvrnss 7117 . . . . . . . . . . 11 ((◑𝐽 Fn (π‘Ž Γ— π‘Ž) ∧ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž) β†’ ran ◑𝐽 βŠ† π‘Ž)
234 ssdomg 8993 . . . . . . . . . . 11 (π‘Ž ∈ V β†’ (ran ◑𝐽 βŠ† π‘Ž β†’ ran ◑𝐽 β‰Ό π‘Ž))
23514, 233, 234mpsyl 68 . . . . . . . . . 10 ((◑𝐽 Fn (π‘Ž Γ— π‘Ž) ∧ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž) β†’ ran ◑𝐽 β‰Ό π‘Ž)
23645, 232, 235syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ ran ◑𝐽 β‰Ό π‘Ž)
237 endomtr 9005 . . . . . . . . 9 (((π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽 ∧ ran ◑𝐽 β‰Ό π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
23843, 236, 237syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
23913, 238sylbir 234 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
240 df1o2 8470 . . . . . . . . . . . 12 1o = {βˆ…}
241 1onn 8636 . . . . . . . . . . . 12 1o ∈ Ο‰
242240, 241eqeltrri 2831 . . . . . . . . . . 11 {βˆ…} ∈ Ο‰
243 nnsdom 9646 . . . . . . . . . . 11 ({βˆ…} ∈ Ο‰ β†’ {βˆ…} β‰Ί Ο‰)
244 sdomdom 8973 . . . . . . . . . . 11 ({βˆ…} β‰Ί Ο‰ β†’ {βˆ…} β‰Ό Ο‰)
245242, 243, 244mp2b 10 . . . . . . . . . 10 {βˆ…} β‰Ό Ο‰
246 domtr 9000 . . . . . . . . . 10 (({βˆ…} β‰Ό Ο‰ ∧ Ο‰ β‰Ό π‘Ž) β†’ {βˆ…} β‰Ό π‘Ž)
247245, 191, 246sylancr 588 . . . . . . . . 9 (Ο‰ βŠ† π‘Ž β†’ {βˆ…} β‰Ό π‘Ž)
248 0ex 5307 . . . . . . . . . . . 12 βˆ… ∈ V
24914, 248xpsnen 9052 . . . . . . . . . . 11 (π‘Ž Γ— {βˆ…}) β‰ˆ π‘Ž
250249ensymi 8997 . . . . . . . . . 10 π‘Ž β‰ˆ (π‘Ž Γ— {βˆ…})
25114xpdom2 9064 . . . . . . . . . 10 ({βˆ…} β‰Ό π‘Ž β†’ (π‘Ž Γ— {βˆ…}) β‰Ό (π‘Ž Γ— π‘Ž))
252 endomtr 9005 . . . . . . . . . 10 ((π‘Ž β‰ˆ (π‘Ž Γ— {βˆ…}) ∧ (π‘Ž Γ— {βˆ…}) β‰Ό (π‘Ž Γ— π‘Ž)) β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
253250, 251, 252sylancr 588 . . . . . . . . 9 ({βˆ…} β‰Ό π‘Ž β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
254247, 253syl 17 . . . . . . . 8 (Ο‰ βŠ† π‘Ž β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
255254ad2antrl 727 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
256 sbth 9090 . . . . . . 7 (((π‘Ž Γ— π‘Ž) β‰Ό π‘Ž ∧ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
257239, 255, 256syl2anc 585 . . . . . 6 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
258257expr 458 . . . . 5 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
259 simplr 768 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
260 simpll 766 . . . . . . . . 9 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž ∈ On)
261 simprr 772 . . . . . . . . 9 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
262 rexnal 3101 . . . . . . . . . 10 (βˆƒπ‘š ∈ π‘Ž Β¬ π‘š β‰Ί π‘Ž ↔ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
263 onelss 6404 . . . . . . . . . . . . 13 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ π‘š βŠ† π‘Ž))
264 ssdomg 8993 . . . . . . . . . . . . 13 (π‘Ž ∈ On β†’ (π‘š βŠ† π‘Ž β†’ π‘š β‰Ό π‘Ž))
265263, 264syld 47 . . . . . . . . . . . 12 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ π‘š β‰Ό π‘Ž))
266 bren2 8976 . . . . . . . . . . . . 13 (π‘š β‰ˆ π‘Ž ↔ (π‘š β‰Ό π‘Ž ∧ Β¬ π‘š β‰Ί π‘Ž))
267266simplbi2 502 . . . . . . . . . . . 12 (π‘š β‰Ό π‘Ž β†’ (Β¬ π‘š β‰Ί π‘Ž β†’ π‘š β‰ˆ π‘Ž))
268265, 267syl6 35 . . . . . . . . . . 11 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ (Β¬ π‘š β‰Ί π‘Ž β†’ π‘š β‰ˆ π‘Ž)))
269268reximdvai 3166 . . . . . . . . . 10 (π‘Ž ∈ On β†’ (βˆƒπ‘š ∈ π‘Ž Β¬ π‘š β‰Ί π‘Ž β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž))
270262, 269biimtrrid 242 . . . . . . . . 9 (π‘Ž ∈ On β†’ (Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž))
271260, 261, 270sylc 65 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž)
272 r19.29 3115 . . . . . . . 8 ((βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž) β†’ βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž))
273259, 271, 272syl2anc 585 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž))
274 simprl 770 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
275 onelon 6387 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ π‘š ∈ On)
276 ensym 8996 . . . . . . . . . . . . . . . . . 18 (π‘š β‰ˆ π‘Ž β†’ π‘Ž β‰ˆ π‘š)
277 domentr 9006 . . . . . . . . . . . . . . . . . 18 ((Ο‰ β‰Ό π‘Ž ∧ π‘Ž β‰ˆ π‘š) β†’ Ο‰ β‰Ό π‘š)
278191, 276, 277syl2an 597 . . . . . . . . . . . . . . . . 17 ((Ο‰ βŠ† π‘Ž ∧ π‘š β‰ˆ π‘Ž) β†’ Ο‰ β‰Ό π‘š)
279 domnsym 9096 . . . . . . . . . . . . . . . . . . 19 (Ο‰ β‰Ό π‘š β†’ Β¬ π‘š β‰Ί Ο‰)
280 nnsdom 9646 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ Ο‰ β†’ π‘š β‰Ί Ο‰)
281279, 280nsyl 140 . . . . . . . . . . . . . . . . . 18 (Ο‰ β‰Ό π‘š β†’ Β¬ π‘š ∈ Ο‰)
282 ontri1 6396 . . . . . . . . . . . . . . . . . . 19 ((Ο‰ ∈ On ∧ π‘š ∈ On) β†’ (Ο‰ βŠ† π‘š ↔ Β¬ π‘š ∈ Ο‰))
283199, 282mpan 689 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ On β†’ (Ο‰ βŠ† π‘š ↔ Β¬ π‘š ∈ Ο‰))
284281, 283imbitrrid 245 . . . . . . . . . . . . . . . . 17 (π‘š ∈ On β†’ (Ο‰ β‰Ό π‘š β†’ Ο‰ βŠ† π‘š))
285275, 278, 284syl2im 40 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ ((Ο‰ βŠ† π‘Ž ∧ π‘š β‰ˆ π‘Ž) β†’ Ο‰ βŠ† π‘š))
286285expd 417 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ (Ο‰ βŠ† π‘Ž β†’ (π‘š β‰ˆ π‘Ž β†’ Ο‰ βŠ† π‘š)))
287286impcom 409 . . . . . . . . . . . . . 14 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ (π‘š β‰ˆ π‘Ž β†’ Ο‰ βŠ† π‘š))
288287imim1d 82 . . . . . . . . . . . . 13 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘š β‰ˆ π‘Ž β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)))
289288imp32 420 . . . . . . . . . . . 12 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)
290 entr 8999 . . . . . . . . . . . . . . . 16 (((π‘š Γ— π‘š) β‰ˆ π‘š ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘š Γ— π‘š) β‰ˆ π‘Ž)
291290ancoms 460 . . . . . . . . . . . . . . 15 ((π‘š β‰ˆ π‘Ž ∧ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘š Γ— π‘š) β‰ˆ π‘Ž)
292 xpen 9137 . . . . . . . . . . . . . . . . 17 ((π‘Ž β‰ˆ π‘š ∧ π‘Ž β‰ˆ π‘š) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š))
293292anidms 568 . . . . . . . . . . . . . . . 16 (π‘Ž β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š))
294 entr 8999 . . . . . . . . . . . . . . . 16 (((π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š) ∧ (π‘š Γ— π‘š) β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
295293, 294sylan 581 . . . . . . . . . . . . . . 15 ((π‘Ž β‰ˆ π‘š ∧ (π‘š Γ— π‘š) β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
296276, 291, 295syl2an2r 684 . . . . . . . . . . . . . 14 ((π‘š β‰ˆ π‘Ž ∧ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
297296ex 414 . . . . . . . . . . . . 13 (π‘š β‰ˆ π‘Ž β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
298297ad2antll 728 . . . . . . . . . . . 12 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
299289, 298mpd 15 . . . . . . . . . . 11 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
300299ex 414 . . . . . . . . . 10 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ (((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
301300expr 458 . . . . . . . . 9 ((Ο‰ βŠ† π‘Ž ∧ π‘Ž ∈ On) β†’ (π‘š ∈ π‘Ž β†’ (((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)))
302301rexlimdv 3154 . . . . . . . 8 ((Ο‰ βŠ† π‘Ž ∧ π‘Ž ∈ On) β†’ (βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
303274, 260, 302syl2anc 585 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
304273, 303mpd 15 . . . . . 6 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
305304expr 458 . . . . 5 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
306258, 305pm2.61d 179 . . . 4 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
307306exp31 421 . . 3 (π‘Ž ∈ On β†’ (βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)))
3086, 12, 307tfis3 7844 . 2 (𝐴 ∈ On β†’ (Ο‰ βŠ† 𝐴 β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴))
309308imp 408 1 ((𝐴 ∈ On ∧ Ο‰ βŠ† 𝐴) β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634   class class class wbr 5148  {copab 5210   E cep 5579   Se wse 5629   We wwe 5630   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364   Fn wfn 6536  βŸΆwf 6537  β€“1-1β†’wf1 6538  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541   Isom wiso 6542  Ο‰com 7852  1st c1st 7970  2nd c2nd 7971  1oc1o 8456   β‰ˆ cen 8933   β‰Ό cdom 8934   β‰Ί csdm 8935  Fincfn 8936  OrdIsocoi 9501  cardccrd 9927
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 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-oi 9502  df-card 9931
This theorem is referenced by:  infxpen  10006
  Copyright terms: Public domain W3C validator