MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infxpenlem Structured version   Visualization version   GIF version
Theorem infxpenlem 10004
Description: Lemma for infxpen 10005. (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 4000 . . . 4 (π‘Ž = π‘š β†’ (Ο‰ βŠ† π‘Ž ↔ Ο‰ βŠ† π‘š))
2 xpeq12 5691 . . . . . 6 ((π‘Ž = π‘š ∧ π‘Ž = π‘š) β†’ (π‘Ž Γ— π‘Ž) = (π‘š Γ— π‘š))
32anidms 566 . . . . 5 (π‘Ž = π‘š β†’ (π‘Ž Γ— π‘Ž) = (π‘š Γ— π‘š))
4 id 22 . . . . 5 (π‘Ž = π‘š β†’ π‘Ž = π‘š)
53, 4breq12d 5151 . . . 4 (π‘Ž = π‘š β†’ ((π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž ↔ (π‘š Γ— π‘š) β‰ˆ π‘š))
61, 5imbi12d 344 . . 3 (π‘Ž = π‘š β†’ ((Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž) ↔ (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)))
7 sseq2 4000 . . . 4 (π‘Ž = 𝐴 β†’ (Ο‰ βŠ† π‘Ž ↔ Ο‰ βŠ† 𝐴))
8 xpeq12 5691 . . . . . 6 ((π‘Ž = 𝐴 ∧ π‘Ž = 𝐴) β†’ (π‘Ž Γ— π‘Ž) = (𝐴 Γ— 𝐴))
98anidms 566 . . . . 5 (π‘Ž = 𝐴 β†’ (π‘Ž Γ— π‘Ž) = (𝐴 Γ— 𝐴))
10 id 22 . . . . 5 (π‘Ž = 𝐴 β†’ π‘Ž = 𝐴)
119, 10breq12d 5151 . . . 4 (π‘Ž = 𝐴 β†’ ((π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž ↔ (𝐴 Γ— 𝐴) β‰ˆ 𝐴))
127, 11imbi12d 344 . . 3 (π‘Ž = 𝐴 β†’ ((Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž) ↔ (Ο‰ βŠ† 𝐴 β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴)))
13 infxpen.2 . . . . . . . 8 (πœ‘ ↔ ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)))
14 vex 3470 . . . . . . . . . . . . 13 π‘Ž ∈ V
1514, 14xpex 7733 . . . . . . . . . . . 12 (π‘Ž Γ— π‘Ž) ∈ V
16 simpll 764 . . . . . . . . . . . . . . . . . 18 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž ∈ On)
1713, 16sylbi 216 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Ž ∈ On)
18 onss 7765 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ On β†’ π‘Ž βŠ† On)
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘Ž βŠ† On)
20 xpss12 5681 . . . . . . . . . . . . . . . 16 ((π‘Ž βŠ† On ∧ π‘Ž βŠ† On) β†’ (π‘Ž Γ— π‘Ž) βŠ† (On Γ— On))
2119, 19, 20syl2anc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘Ž Γ— π‘Ž) βŠ† (On Γ— On))
22 leweon.1 . . . . . . . . . . . . . . . . 17 𝐿 = {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (On Γ— On) ∧ 𝑦 ∈ (On Γ— On)) ∧ ((1st β€˜π‘₯) ∈ (1st β€˜π‘¦) ∨ ((1st β€˜π‘₯) = (1st β€˜π‘¦) ∧ (2nd β€˜π‘₯) ∈ (2nd β€˜π‘¦))))}
23 r0weon.1 . . . . . . . . . . . . . . . . 17 𝑅 = {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))}
2422, 23r0weon 10003 . . . . . . . . . . . . . . . 16 (𝑅 We (On Γ— On) ∧ 𝑅 Se (On Γ— On))
2524simpli 483 . . . . . . . . . . . . . . 15 𝑅 We (On Γ— On)
26 wess 5653 . . . . . . . . . . . . . . 15 ((π‘Ž Γ— π‘Ž) βŠ† (On Γ— On) β†’ (𝑅 We (On Γ— On) β†’ 𝑅 We (π‘Ž Γ— π‘Ž)))
2721, 25, 26mpisyl 21 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 We (π‘Ž Γ— π‘Ž))
28 weinxp 5750 . . . . . . . . . . . . . 14 (𝑅 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
2927, 28sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
30 infxpen.1 . . . . . . . . . . . . . 14 𝑄 = (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))
31 weeq1 5654 . . . . . . . . . . . . . 14 (𝑄 = (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) β†’ (𝑄 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž)))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 (𝑄 We (π‘Ž Γ— π‘Ž) ↔ (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) We (π‘Ž Γ— π‘Ž))
3329, 32sylibr 233 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 We (π‘Ž Γ— π‘Ž))
34 infxpen.4 . . . . . . . . . . . . 13 𝐽 = OrdIso(𝑄, (π‘Ž Γ— π‘Ž))
3534oiiso 9528 . . . . . . . . . . . 12 (((π‘Ž Γ— π‘Ž) ∈ V ∧ 𝑄 We (π‘Ž Γ— π‘Ž)) β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
3615, 33, 35sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
37 isof1o 7312 . . . . . . . . . . 11 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ 𝐽:dom 𝐽–1-1-ontoβ†’(π‘Ž Γ— π‘Ž))
38 f1ocnv 6835 . . . . . . . . . . 11 (𝐽:dom 𝐽–1-1-ontoβ†’(π‘Ž Γ— π‘Ž) β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽)
39 f1of1 6822 . . . . . . . . . . 11 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
4036, 37, 38, 394syl 19 . . . . . . . . . 10 (πœ‘ β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
41 f1f1orn 6834 . . . . . . . . . 10 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’ran ◑𝐽)
4215f1oen 8965 . . . . . . . . . 10 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’ran ◑𝐽 β†’ (π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽)
4340, 41, 423syl 18 . . . . . . . . 9 (πœ‘ β†’ (π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽)
44 f1ofn 6824 . . . . . . . . . . 11 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽 Fn (π‘Ž Γ— π‘Ž))
4536, 37, 38, 444syl 19 . . . . . . . . . 10 (πœ‘ β†’ ◑𝐽 Fn (π‘Ž Γ— π‘Ž))
4636adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)))
4737, 38, 393syl 18 . . . . . . . . . . . . . . . . . 18 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽)
48 cnvimass 6070 . . . . . . . . . . . . . . . . . . 19 (◑𝑄 β€œ {𝑀}) βŠ† dom 𝑄
49 inss2 4221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
5030, 49eqsstri 4008 . . . . . . . . . . . . . . . . . . . . 21 𝑄 βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
51 dmss 5892 . . . . . . . . . . . . . . . . . . . . 21 (𝑄 βŠ† ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) β†’ dom 𝑄 βŠ† dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 dom 𝑄 βŠ† dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))
53 dmxpid 5919 . . . . . . . . . . . . . . . . . . . 20 dom ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) = (π‘Ž Γ— π‘Ž)
5452, 53sseqtri 4010 . . . . . . . . . . . . . . . . . . 19 dom 𝑄 βŠ† (π‘Ž Γ— π‘Ž)
5548, 54sstri 3983 . . . . . . . . . . . . . . . . . 18 (◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž)
56 f1ores 6837 . . . . . . . . . . . . . . . . . 18 ((◑𝐽:(π‘Ž Γ— π‘Ž)–1-1β†’dom 𝐽 ∧ (◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
5747, 55, 56sylancl 585 . . . . . . . . . . . . . . . . 17 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
5815, 15xpex 7733 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)) ∈ V
5958inex2 5308 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))) ∈ V
6030, 59eqeltri 2821 . . . . . . . . . . . . . . . . . . . 20 𝑄 ∈ V
6160cnvex 7909 . . . . . . . . . . . . . . . . . . 19 ◑𝑄 ∈ V
6261imaex 7900 . . . . . . . . . . . . . . . . . 18 (◑𝑄 β€œ {𝑀}) ∈ V
6362f1oen 8965 . . . . . . . . . . . . . . . . 17 ((◑𝐽 β†Ύ (◑𝑄 β€œ {𝑀})):(◑𝑄 β€œ {𝑀})–1-1-ontoβ†’(◑𝐽 β€œ (◑𝑄 β€œ {𝑀})) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
6446, 57, 633syl 18 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})))
65 sseqin2 4207 . . . . . . . . . . . . . . . . . . 19 ((◑𝑄 β€œ {𝑀}) βŠ† (π‘Ž Γ— π‘Ž) ↔ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀})) = (◑𝑄 β€œ {𝑀}))
6655, 65mpbi 229 . . . . . . . . . . . . . . . . . 18 ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀})) = (◑𝑄 β€œ {𝑀})
6766imaeq2i 6047 . . . . . . . . . . . . . . . . 17 (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (◑𝐽 β€œ (◑𝑄 β€œ {𝑀}))
68 isocnv 7319 . . . . . . . . . . . . . . . . . . . 20 (𝐽 Isom E , 𝑄 (dom 𝐽, (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽))
6946, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽))
70 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝑀 ∈ (π‘Ž Γ— π‘Ž))
71 isoini 7327 . . . . . . . . . . . . . . . . . . 19 ((◑𝐽 Isom 𝑄, E ((π‘Ž Γ— π‘Ž), dom 𝐽) ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})))
7269, 70, 71syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})))
73 fvex 6894 . . . . . . . . . . . . . . . . . . . . 21 (β—‘π½β€˜π‘€) ∈ V
7473epini 6085 . . . . . . . . . . . . . . . . . . . 20 (β—‘ E β€œ {(β—‘π½β€˜π‘€)}) = (β—‘π½β€˜π‘€)
7574ineq2i 4201 . . . . . . . . . . . . . . . . . . 19 (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})) = (dom 𝐽 ∩ (β—‘π½β€˜π‘€))
7634oicl 9520 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐽
77 f1of 6823 . . . . . . . . . . . . . . . . . . . . . . 23 (◑𝐽:(π‘Ž Γ— π‘Ž)–1-1-ontoβ†’dom 𝐽 β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)⟢dom 𝐽)
7836, 37, 38, 774syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ◑𝐽:(π‘Ž Γ— π‘Ž)⟢dom 𝐽)
7978ffvelcdmda 7076 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ dom 𝐽)
80 ordelss 6370 . . . . . . . . . . . . . . . . . . . . 21 ((Ord dom 𝐽 ∧ (β—‘π½β€˜π‘€) ∈ dom 𝐽) β†’ (β—‘π½β€˜π‘€) βŠ† dom 𝐽)
8176, 79, 80sylancr 586 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) βŠ† dom 𝐽)
82 sseqin2 4207 . . . . . . . . . . . . . . . . . . . 20 ((β—‘π½β€˜π‘€) βŠ† dom 𝐽 ↔ (dom 𝐽 ∩ (β—‘π½β€˜π‘€)) = (β—‘π½β€˜π‘€))
8381, 82sylib 217 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (dom 𝐽 ∩ (β—‘π½β€˜π‘€)) = (β—‘π½β€˜π‘€))
8475, 83eqtrid 2776 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (dom 𝐽 ∩ (β—‘ E β€œ {(β—‘π½β€˜π‘€)})) = (β—‘π½β€˜π‘€))
8572, 84eqtrd 2764 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ ((π‘Ž Γ— π‘Ž) ∩ (◑𝑄 β€œ {𝑀}))) = (β—‘π½β€˜π‘€))
8667, 85eqtr3id 2778 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝐽 β€œ (◑𝑄 β€œ {𝑀})) = (β—‘π½β€˜π‘€))
8764, 86breqtrd 5164 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰ˆ (β—‘π½β€˜π‘€))
8887ensymd 8997 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) β‰ˆ (◑𝑄 β€œ {𝑀}))
89 infxpen.3 . . . . . . . . . . . . . . . . . . 19 𝑀 = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))
90 fvex 6894 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜π‘€) ∈ V
91 fvex 6894 . . . . . . . . . . . . . . . . . . . 20 (2nd β€˜π‘€) ∈ V
9290, 91unex 7726 . . . . . . . . . . . . . . . . . . 19 ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ V
9389, 92eqeltri 2821 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
9493sucex 7787 . . . . . . . . . . . . . . . . 17 suc 𝑀 ∈ V
9594, 94xpex 7733 . . . . . . . . . . . . . . . 16 (suc 𝑀 Γ— suc 𝑀) ∈ V
96 xpss 5682 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž Γ— π‘Ž) βŠ† (V Γ— V)
97 simp3 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (◑𝑄 β€œ {𝑀}))
98 vex 3470 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
9998eliniseg 6083 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ V β†’ (𝑧 ∈ (◑𝑄 β€œ {𝑀}) ↔ 𝑧𝑄𝑀))
10099elv 3472 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (◑𝑄 β€œ {𝑀}) ↔ 𝑧𝑄𝑀)
10197, 100sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧𝑄𝑀)
10230breqi 5144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑄𝑀 ↔ 𝑧(𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))𝑀)
103 brin 5190 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧(𝑅 ∩ ((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž)))𝑀 ↔ (𝑧𝑅𝑀 ∧ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀))
104102, 103bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑄𝑀 ↔ (𝑧𝑅𝑀 ∧ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀))
105104simprbi 496 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑀 β†’ 𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀)
106 brxp 5715 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀 ↔ (𝑧 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)))
107106simplbi 497 . . . . . . . . . . . . . . . . . . . . 21 (𝑧((π‘Ž Γ— π‘Ž) Γ— (π‘Ž Γ— π‘Ž))𝑀 β†’ 𝑧 ∈ (π‘Ž Γ— π‘Ž))
108101, 105, 1073syl 18 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (π‘Ž Γ— π‘Ž))
10996, 108sselid 3972 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (V Γ— V))
11017adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ π‘Ž ∈ On)
1111103adant3 1129 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ π‘Ž ∈ On)
112 xp1st 8000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (π‘Ž Γ— π‘Ž) β†’ (1st β€˜π‘§) ∈ π‘Ž)
113 onelon 6379 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ (1st β€˜π‘§) ∈ π‘Ž) β†’ (1st β€˜π‘§) ∈ On)
114112, 113sylan2 592 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ On ∧ 𝑧 ∈ (π‘Ž Γ— π‘Ž)) β†’ (1st β€˜π‘§) ∈ On)
115111, 108, 114syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) ∈ On)
116 eloni 6364 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž ∈ On β†’ Ord π‘Ž)
117 elxp7 8003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ (π‘Ž Γ— π‘Ž) ↔ (𝑀 ∈ (V Γ— V) ∧ ((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž)))
118117simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ (π‘Ž Γ— π‘Ž) β†’ ((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž))
119 ordunel 7808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord π‘Ž ∧ (1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž)
1201193expib 1119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord π‘Ž β†’ (((1st β€˜π‘€) ∈ π‘Ž ∧ (2nd β€˜π‘€) ∈ π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž))
121116, 118, 120syl2im 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ On β†’ (𝑀 ∈ (π‘Ž Γ— π‘Ž) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž))
122110, 70, 121sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∈ π‘Ž)
12389, 122eqeltrid 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ 𝑀 ∈ π‘Ž)
124 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
12513, 124sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
126 simprl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
12713, 126sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ Ο‰ βŠ† π‘Ž)
128 iscard 9966 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((cardβ€˜π‘Ž) = π‘Ž ↔ (π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž))
129 cardlim 9963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Lim (cardβ€˜π‘Ž))
130 sseq2 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Ο‰ βŠ† π‘Ž))
131 limeq 6366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Lim (cardβ€˜π‘Ž) ↔ Lim π‘Ž))
132130, 131bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((cardβ€˜π‘Ž) = π‘Ž β†’ ((Ο‰ βŠ† (cardβ€˜π‘Ž) ↔ Lim (cardβ€˜π‘Ž)) ↔ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž)))
133129, 132mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((cardβ€˜π‘Ž) = π‘Ž β†’ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž))
134128, 133sylbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) β†’ (Ο‰ βŠ† π‘Ž ↔ Lim π‘Ž))
135134biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) ∧ Ο‰ βŠ† π‘Ž) β†’ Lim π‘Ž)
13617, 125, 127, 135syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ Lim π‘Ž)
137136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ Lim π‘Ž)
138 limsuc 7831 . . . . . . . . . . . . . . . . . . . . . . . 24 (Lim π‘Ž β†’ (𝑀 ∈ π‘Ž ↔ suc 𝑀 ∈ π‘Ž))
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (𝑀 ∈ π‘Ž ↔ suc 𝑀 ∈ π‘Ž))
140123, 139mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 ∈ π‘Ž)
141 onelon 6379 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ suc 𝑀 ∈ π‘Ž) β†’ suc 𝑀 ∈ On)
14217, 140, 141syl2an2r 682 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 ∈ On)
1431423adant3 1129 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ suc 𝑀 ∈ On)
144 ssun1 4164 . . . . . . . . . . . . . . . . . . . . 21 (1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§))
145144a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
146104simplbi 497 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑄𝑀 β†’ 𝑧𝑅𝑀)
147 df-br 5139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑅𝑀 ↔ βŸ¨π‘§, π‘€βŸ© ∈ 𝑅)
14823eleq2i 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βŸ¨π‘§, π‘€βŸ© ∈ 𝑅 ↔ βŸ¨π‘§, π‘€βŸ© ∈ {βŸ¨π‘§, π‘€βŸ© ∣ ((𝑧 ∈ (On Γ— On) ∧ 𝑀 ∈ (On Γ— On)) ∧ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))})
149 opabidw 5514 . . . . . . . . . . . . . . . . . . . . . . . . . 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 496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧𝑅𝑀 β†’ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∨ (((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀)))
152 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) ∧ 𝑧𝐿𝑀) β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
153152orim2i 907 . . . . . . . . . . . . . . . . . . . . . . . 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 6894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1st β€˜π‘§) ∈ V
156 fvex 6894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd β€˜π‘§) ∈ V
157155, 156unex 7726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ V
158157elsuc 6424 . . . . . . . . . . . . . . . . . . . . . . 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 6420 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 = ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)) β†’ suc 𝑀 = suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€)))
16189, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑀 = suc ((1st β€˜π‘€) βˆͺ (2nd β€˜π‘€))
162159, 161eleqtrrdi 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑅𝑀 β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)
163101, 146, 1623syl 18 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)
164 ontr2 6401 . . . . . . . . . . . . . . . . . . . . 21 (((1st β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) β†’ (((1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀) β†’ (1st β€˜π‘§) ∈ suc 𝑀))
165164imp 406 . . . . . . . . . . . . . . . . . . . 20 ((((1st β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((1st β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)) β†’ (1st β€˜π‘§) ∈ suc 𝑀)
166115, 143, 145, 163, 165syl22anc 836 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (1st β€˜π‘§) ∈ suc 𝑀)
167 xp2nd 8001 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (π‘Ž Γ— π‘Ž) β†’ (2nd β€˜π‘§) ∈ π‘Ž)
168 onelon 6379 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž ∈ On ∧ (2nd β€˜π‘§) ∈ π‘Ž) β†’ (2nd β€˜π‘§) ∈ On)
169167, 168sylan2 592 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ On ∧ 𝑧 ∈ (π‘Ž Γ— π‘Ž)) β†’ (2nd β€˜π‘§) ∈ On)
170111, 108, 169syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) ∈ On)
171 ssun2 4165 . . . . . . . . . . . . . . . . . . . . 21 (2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§))
172171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)))
173 ontr2 6401 . . . . . . . . . . . . . . . . . . . . 21 (((2nd β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) β†’ (((2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀) β†’ (2nd β€˜π‘§) ∈ suc 𝑀))
174173imp 406 . . . . . . . . . . . . . . . . . . . 20 ((((2nd β€˜π‘§) ∈ On ∧ suc 𝑀 ∈ On) ∧ ((2nd β€˜π‘§) βŠ† ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∧ ((1st β€˜π‘§) βˆͺ (2nd β€˜π‘§)) ∈ suc 𝑀)) β†’ (2nd β€˜π‘§) ∈ suc 𝑀)
175170, 143, 172, 163, 174syl22anc 836 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ (2nd β€˜π‘§) ∈ suc 𝑀)
176 elxp7 8003 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (suc 𝑀 Γ— suc 𝑀) ↔ (𝑧 ∈ (V Γ— V) ∧ ((1st β€˜π‘§) ∈ suc 𝑀 ∧ (2nd β€˜π‘§) ∈ suc 𝑀)))
177176biimpri 227 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (V Γ— V) ∧ ((1st β€˜π‘§) ∈ suc 𝑀 ∧ (2nd β€˜π‘§) ∈ suc 𝑀)) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀))
178109, 166, 175, 177syl12anc 834 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž) ∧ 𝑧 ∈ (◑𝑄 β€œ {𝑀})) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀))
1791783expia 1118 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (𝑧 ∈ (◑𝑄 β€œ {𝑀}) β†’ 𝑧 ∈ (suc 𝑀 Γ— suc 𝑀)))
180179ssrdv 3980 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) βŠ† (suc 𝑀 Γ— suc 𝑀))
181 ssdomg 8992 . . . . . . . . . . . . . . . 16 ((suc 𝑀 Γ— suc 𝑀) ∈ V β†’ ((◑𝑄 β€œ {𝑀}) βŠ† (suc 𝑀 Γ— suc 𝑀) β†’ (◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀)))
18295, 180, 181mpsyl 68 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀))
183127adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
184 nnfi 9163 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Ο‰ β†’ suc 𝑀 ∈ Fin)
185 xpfi 9313 . . . . . . . . . . . . . . . . . . . . . 22 ((suc 𝑀 ∈ Fin ∧ suc 𝑀 ∈ Fin) β†’ (suc 𝑀 Γ— suc 𝑀) ∈ Fin)
186185anidms 566 . . . . . . . . . . . . . . . . . . . . 21 (suc 𝑀 ∈ Fin β†’ (suc 𝑀 Γ— suc 𝑀) ∈ Fin)
187 isfinite 9643 . . . . . . . . . . . . . . . . . . . . 21 ((suc 𝑀 Γ— suc 𝑀) ∈ Fin ↔ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
188186, 187sylib 217 . . . . . . . . . . . . . . . . . . . 20 (suc 𝑀 ∈ Fin β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
189184, 188syl 17 . . . . . . . . . . . . . . . . . . 19 (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰)
190 ssdomg 8992 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž ∈ V β†’ (Ο‰ βŠ† π‘Ž β†’ Ο‰ β‰Ό π‘Ž))
191190elv 3472 . . . . . . . . . . . . . . . . . . 19 (Ο‰ βŠ† π‘Ž β†’ Ο‰ β‰Ό π‘Ž)
192 sdomdomtr 9106 . . . . . . . . . . . . . . . . . . 19 (((suc 𝑀 Γ— suc 𝑀) β‰Ί Ο‰ ∧ Ο‰ β‰Ό π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
193189, 191, 192syl2an 595 . . . . . . . . . . . . . . . . . 18 ((suc 𝑀 ∈ Ο‰ ∧ Ο‰ βŠ† π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
194193expcom 413 . . . . . . . . . . . . . . . . 17 (Ο‰ βŠ† π‘Ž β†’ (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
195183, 194syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
196 breq1 5141 . . . . . . . . . . . . . . . . . 18 (π‘š = suc 𝑀 β†’ (π‘š β‰Ί π‘Ž ↔ suc 𝑀 β‰Ί π‘Ž))
197125adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
198196, 197, 140rspcdva 3605 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ suc 𝑀 β‰Ί π‘Ž)
199 omelon 9637 . . . . . . . . . . . . . . . . . . 19 Ο‰ ∈ On
200 ontri1 6388 . . . . . . . . . . . . . . . . . . 19 ((Ο‰ ∈ On ∧ suc 𝑀 ∈ On) β†’ (Ο‰ βŠ† suc 𝑀 ↔ Β¬ suc 𝑀 ∈ Ο‰))
201199, 142, 200sylancr 586 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Ο‰ βŠ† suc 𝑀 ↔ Β¬ suc 𝑀 ∈ Ο‰))
202 sseq2 4000 . . . . . . . . . . . . . . . . . . . 20 (π‘š = suc 𝑀 β†’ (Ο‰ βŠ† π‘š ↔ Ο‰ βŠ† suc 𝑀))
203 xpeq12 5691 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘š = suc 𝑀 ∧ π‘š = suc 𝑀) β†’ (π‘š Γ— π‘š) = (suc 𝑀 Γ— suc 𝑀))
204203anidms 566 . . . . . . . . . . . . . . . . . . . . 21 (π‘š = suc 𝑀 β†’ (π‘š Γ— π‘š) = (suc 𝑀 Γ— suc 𝑀))
205 id 22 . . . . . . . . . . . . . . . . . . . . 21 (π‘š = suc 𝑀 β†’ π‘š = suc 𝑀)
206204, 205breq12d 5151 . . . . . . . . . . . . . . . . . . . 20 (π‘š = suc 𝑀 β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š ↔ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
207202, 206imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (π‘š = suc 𝑀 β†’ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ↔ (Ο‰ βŠ† suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀)))
208 simplr 766 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
20913, 208sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
210209adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
211207, 210, 140rspcdva 3605 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Ο‰ βŠ† suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
212201, 211sylbird 260 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Β¬ suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀))
213 ensdomtr 9109 . . . . . . . . . . . . . . . . . 18 (((suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀 ∧ suc 𝑀 β‰Ί π‘Ž) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
214213expcom 413 . . . . . . . . . . . . . . . . 17 (suc 𝑀 β‰Ί π‘Ž β†’ ((suc 𝑀 Γ— suc 𝑀) β‰ˆ suc 𝑀 β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
215198, 212, 214sylsyld 61 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (Β¬ suc 𝑀 ∈ Ο‰ β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž))
216195, 215pm2.61d 179 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž)
217 domsdomtr 9108 . . . . . . . . . . . . . . 15 (((◑𝑄 β€œ {𝑀}) β‰Ό (suc 𝑀 Γ— suc 𝑀) ∧ (suc 𝑀 Γ— suc 𝑀) β‰Ί π‘Ž) β†’ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž)
218182, 216, 217syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž)
219 ensdomtr 9109 . . . . . . . . . . . . . 14 (((β—‘π½β€˜π‘€) β‰ˆ (◑𝑄 β€œ {𝑀}) ∧ (◑𝑄 β€œ {𝑀}) β‰Ί π‘Ž) β†’ (β—‘π½β€˜π‘€) β‰Ί π‘Ž)
22088, 218, 219syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) β‰Ί π‘Ž)
221 ordelon 6378 . . . . . . . . . . . . . . 15 ((Ord dom 𝐽 ∧ (β—‘π½β€˜π‘€) ∈ dom 𝐽) β†’ (β—‘π½β€˜π‘€) ∈ On)
22276, 79, 221sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ On)
223 onenon 9940 . . . . . . . . . . . . . . 15 (π‘Ž ∈ On β†’ π‘Ž ∈ dom card)
224110, 223syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ π‘Ž ∈ dom card)
225 cardsdomel 9965 . . . . . . . . . . . . . 14 (((β—‘π½β€˜π‘€) ∈ On ∧ π‘Ž ∈ dom card) β†’ ((β—‘π½β€˜π‘€) β‰Ί π‘Ž ↔ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž)))
226222, 224, 225syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((β—‘π½β€˜π‘€) β‰Ί π‘Ž ↔ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž)))
227220, 226mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž))
228 eleq2 2814 . . . . . . . . . . . . . 14 ((cardβ€˜π‘Ž) = π‘Ž β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
229128, 228sylbir 234 . . . . . . . . . . . . 13 ((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž) β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
23017, 197, 229syl2an2r 682 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ ((β—‘π½β€˜π‘€) ∈ (cardβ€˜π‘Ž) ↔ (β—‘π½β€˜π‘€) ∈ π‘Ž))
231227, 230mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ (π‘Ž Γ— π‘Ž)) β†’ (β—‘π½β€˜π‘€) ∈ π‘Ž)
232231ralrimiva 3138 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž)
233 fnfvrnss 7112 . . . . . . . . . . 11 ((◑𝐽 Fn (π‘Ž Γ— π‘Ž) ∧ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž) β†’ ran ◑𝐽 βŠ† π‘Ž)
234 ssdomg 8992 . . . . . . . . . . 11 (π‘Ž ∈ V β†’ (ran ◑𝐽 βŠ† π‘Ž β†’ ran ◑𝐽 β‰Ό π‘Ž))
23514, 233, 234mpsyl 68 . . . . . . . . . 10 ((◑𝐽 Fn (π‘Ž Γ— π‘Ž) ∧ βˆ€π‘€ ∈ (π‘Ž Γ— π‘Ž)(β—‘π½β€˜π‘€) ∈ π‘Ž) β†’ ran ◑𝐽 β‰Ό π‘Ž)
23645, 232, 235syl2anc 583 . . . . . . . . 9 (πœ‘ β†’ ran ◑𝐽 β‰Ό π‘Ž)
237 endomtr 9004 . . . . . . . . 9 (((π‘Ž Γ— π‘Ž) β‰ˆ ran ◑𝐽 ∧ ran ◑𝐽 β‰Ό π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
23843, 236, 237syl2anc 583 . . . . . . . 8 (πœ‘ β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
23913, 238sylbir 234 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰Ό π‘Ž)
240 df1o2 8468 . . . . . . . . . . . 12 1o = {βˆ…}
241 1onn 8635 . . . . . . . . . . . 12 1o ∈ Ο‰
242240, 241eqeltrri 2822 . . . . . . . . . . 11 {βˆ…} ∈ Ο‰
243 nnsdom 9645 . . . . . . . . . . 11 ({βˆ…} ∈ Ο‰ β†’ {βˆ…} β‰Ί Ο‰)
244 sdomdom 8972 . . . . . . . . . . 11 ({βˆ…} β‰Ί Ο‰ β†’ {βˆ…} β‰Ό Ο‰)
245242, 243, 244mp2b 10 . . . . . . . . . 10 {βˆ…} β‰Ό Ο‰
246 domtr 8999 . . . . . . . . . 10 (({βˆ…} β‰Ό Ο‰ ∧ Ο‰ β‰Ό π‘Ž) β†’ {βˆ…} β‰Ό π‘Ž)
247245, 191, 246sylancr 586 . . . . . . . . 9 (Ο‰ βŠ† π‘Ž β†’ {βˆ…} β‰Ό π‘Ž)
248 0ex 5297 . . . . . . . . . . . 12 βˆ… ∈ V
24914, 248xpsnen 9051 . . . . . . . . . . 11 (π‘Ž Γ— {βˆ…}) β‰ˆ π‘Ž
250249ensymi 8996 . . . . . . . . . 10 π‘Ž β‰ˆ (π‘Ž Γ— {βˆ…})
25114xpdom2 9063 . . . . . . . . . 10 ({βˆ…} β‰Ό π‘Ž β†’ (π‘Ž Γ— {βˆ…}) β‰Ό (π‘Ž Γ— π‘Ž))
252 endomtr 9004 . . . . . . . . . 10 ((π‘Ž β‰ˆ (π‘Ž Γ— {βˆ…}) ∧ (π‘Ž Γ— {βˆ…}) β‰Ό (π‘Ž Γ— π‘Ž)) β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
253250, 251, 252sylancr 586 . . . . . . . . 9 ({βˆ…} β‰Ό π‘Ž β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
254247, 253syl 17 . . . . . . . 8 (Ο‰ βŠ† π‘Ž β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
255254ad2antrl 725 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž))
256 sbth 9089 . . . . . . 7 (((π‘Ž Γ— π‘Ž) β‰Ό π‘Ž ∧ π‘Ž β‰Ό (π‘Ž Γ— π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
257239, 255, 256syl2anc 583 . . . . . 6 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
258257expr 456 . . . . 5 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
259 simplr 766 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š))
260 simpll 764 . . . . . . . . 9 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ π‘Ž ∈ On)
261 simprr 770 . . . . . . . . 9 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
262 rexnal 3092 . . . . . . . . . 10 (βˆƒπ‘š ∈ π‘Ž Β¬ π‘š β‰Ί π‘Ž ↔ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)
263 onelss 6396 . . . . . . . . . . . . 13 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ π‘š βŠ† π‘Ž))
264 ssdomg 8992 . . . . . . . . . . . . 13 (π‘Ž ∈ On β†’ (π‘š βŠ† π‘Ž β†’ π‘š β‰Ό π‘Ž))
265263, 264syld 47 . . . . . . . . . . . 12 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ π‘š β‰Ό π‘Ž))
266 bren2 8975 . . . . . . . . . . . . 13 (π‘š β‰ˆ π‘Ž ↔ (π‘š β‰Ό π‘Ž ∧ Β¬ π‘š β‰Ί π‘Ž))
267266simplbi2 500 . . . . . . . . . . . 12 (π‘š β‰Ό π‘Ž β†’ (Β¬ π‘š β‰Ί π‘Ž β†’ π‘š β‰ˆ π‘Ž))
268265, 267syl6 35 . . . . . . . . . . 11 (π‘Ž ∈ On β†’ (π‘š ∈ π‘Ž β†’ (Β¬ π‘š β‰Ί π‘Ž β†’ π‘š β‰ˆ π‘Ž)))
269268reximdvai 3157 . . . . . . . . . 10 (π‘Ž ∈ On β†’ (βˆƒπ‘š ∈ π‘Ž Β¬ π‘š β‰Ί π‘Ž β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž))
270262, 269biimtrrid 242 . . . . . . . . 9 (π‘Ž ∈ On β†’ (Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž))
271260, 261, 270sylc 65 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž)
272 r19.29 3106 . . . . . . . 8 ((βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ βˆƒπ‘š ∈ π‘Ž π‘š β‰ˆ π‘Ž) β†’ βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž))
273259, 271, 272syl2anc 583 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž))
274 simprl 768 . . . . . . . 8 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ Ο‰ βŠ† π‘Ž)
275 onelon 6379 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ π‘š ∈ On)
276 ensym 8995 . . . . . . . . . . . . . . . . . 18 (π‘š β‰ˆ π‘Ž β†’ π‘Ž β‰ˆ π‘š)
277 domentr 9005 . . . . . . . . . . . . . . . . . 18 ((Ο‰ β‰Ό π‘Ž ∧ π‘Ž β‰ˆ π‘š) β†’ Ο‰ β‰Ό π‘š)
278191, 276, 277syl2an 595 . . . . . . . . . . . . . . . . 17 ((Ο‰ βŠ† π‘Ž ∧ π‘š β‰ˆ π‘Ž) β†’ Ο‰ β‰Ό π‘š)
279 domnsym 9095 . . . . . . . . . . . . . . . . . . 19 (Ο‰ β‰Ό π‘š β†’ Β¬ π‘š β‰Ί Ο‰)
280 nnsdom 9645 . . . . . . . . . . . . . . . . . . 19 (π‘š ∈ Ο‰ β†’ π‘š β‰Ί Ο‰)
281279, 280nsyl 140 . . . . . . . . . . . . . . . . . 18 (Ο‰ β‰Ό π‘š β†’ Β¬ π‘š ∈ Ο‰)
282 ontri1 6388 . . . . . . . . . . . . . . . . . . 19 ((Ο‰ ∈ On ∧ π‘š ∈ On) β†’ (Ο‰ βŠ† π‘š ↔ Β¬ π‘š ∈ Ο‰))
283199, 282mpan 687 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ On β†’ (Ο‰ βŠ† π‘š ↔ Β¬ π‘š ∈ Ο‰))
284281, 283imbitrrid 245 . . . . . . . . . . . . . . . . 17 (π‘š ∈ On β†’ (Ο‰ β‰Ό π‘š β†’ Ο‰ βŠ† π‘š))
285275, 278, 284syl2im 40 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ ((Ο‰ βŠ† π‘Ž ∧ π‘š β‰ˆ π‘Ž) β†’ Ο‰ βŠ† π‘š))
286285expd 415 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ On ∧ π‘š ∈ π‘Ž) β†’ (Ο‰ βŠ† π‘Ž β†’ (π‘š β‰ˆ π‘Ž β†’ Ο‰ βŠ† π‘š)))
287286impcom 407 . . . . . . . . . . . . . 14 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ (π‘š β‰ˆ π‘Ž β†’ Ο‰ βŠ† π‘š))
288287imim1d 82 . . . . . . . . . . . . 13 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘š β‰ˆ π‘Ž β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)))
289288imp32 418 . . . . . . . . . . . 12 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)
290 entr 8998 . . . . . . . . . . . . . . . 16 (((π‘š Γ— π‘š) β‰ˆ π‘š ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘š Γ— π‘š) β‰ˆ π‘Ž)
291290ancoms 458 . . . . . . . . . . . . . . 15 ((π‘š β‰ˆ π‘Ž ∧ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘š Γ— π‘š) β‰ˆ π‘Ž)
292 xpen 9136 . . . . . . . . . . . . . . . . 17 ((π‘Ž β‰ˆ π‘š ∧ π‘Ž β‰ˆ π‘š) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š))
293292anidms 566 . . . . . . . . . . . . . . . 16 (π‘Ž β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š))
294 entr 8998 . . . . . . . . . . . . . . . 16 (((π‘Ž Γ— π‘Ž) β‰ˆ (π‘š Γ— π‘š) ∧ (π‘š Γ— π‘š) β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
295293, 294sylan 579 . . . . . . . . . . . . . . 15 ((π‘Ž β‰ˆ π‘š ∧ (π‘š Γ— π‘š) β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
296276, 291, 295syl2an2r 682 . . . . . . . . . . . . . 14 ((π‘š β‰ˆ π‘Ž ∧ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
297296ex 412 . . . . . . . . . . . . 13 (π‘š β‰ˆ π‘Ž β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
298297ad2antll 726 . . . . . . . . . . . 12 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ ((π‘š Γ— π‘š) β‰ˆ π‘š β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
299289, 298mpd 15 . . . . . . . . . . 11 (((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) ∧ ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
300299ex 412 . . . . . . . . . 10 ((Ο‰ βŠ† π‘Ž ∧ (π‘Ž ∈ On ∧ π‘š ∈ π‘Ž)) β†’ (((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
301300expr 456 . . . . . . . . 9 ((Ο‰ βŠ† π‘Ž ∧ π‘Ž ∈ On) β†’ (π‘š ∈ π‘Ž β†’ (((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)))
302301rexlimdv 3145 . . . . . . . 8 ((Ο‰ βŠ† π‘Ž ∧ π‘Ž ∈ On) β†’ (βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
303274, 260, 302syl2anc 583 . . . . . . 7 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (βˆƒπ‘š ∈ π‘Ž ((Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) ∧ π‘š β‰ˆ π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
304273, 303mpd 15 . . . . . 6 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ (Ο‰ βŠ† π‘Ž ∧ Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž)) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
305304expr 456 . . . . 5 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (Β¬ βˆ€π‘š ∈ π‘Ž π‘š β‰Ί π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž))
306258, 305pm2.61d 179 . . . 4 (((π‘Ž ∈ On ∧ βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š)) ∧ Ο‰ βŠ† π‘Ž) β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)
307306exp31 419 . . 3 (π‘Ž ∈ On β†’ (βˆ€π‘š ∈ π‘Ž (Ο‰ βŠ† π‘š β†’ (π‘š Γ— π‘š) β‰ˆ π‘š) β†’ (Ο‰ βŠ† π‘Ž β†’ (π‘Ž Γ— π‘Ž) β‰ˆ π‘Ž)))
3086, 12, 307tfis3 7840 . 2 (𝐴 ∈ On β†’ (Ο‰ βŠ† 𝐴 β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴))
309308imp 406 1 ((𝐴 ∈ On ∧ Ο‰ βŠ† 𝐴) β†’ (𝐴 Γ— 𝐴) β‰ˆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  βˆƒwrex 3062  Vcvv 3466   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  {csn 4620  βŸ¨cop 4626   class class class wbr 5138  {copab 5200   E cep 5569   Se wse 5619   We wwe 5620   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669  Ord word 6353  Oncon0 6354  Lim wlim 6355  suc csuc 6356   Fn wfn 6528  βŸΆwf 6529  β€“1-1β†’wf1 6530  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533   Isom wiso 6534  Ο‰com 7848  1st c1st 7966  2nd c2nd 7967  1oc1o 8454   β‰ˆ cen 8932   β‰Ό cdom 8933   β‰Ί csdm 8934  Fincfn 8935  OrdIsocoi 9500  cardccrd 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-oi 9501  df-card 9930
This theorem is referenced by:  infxpen  10005
  Copyright terms: Public domain W3C validator