MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noetainflem4 Structured version   Visualization version   GIF version
Theorem noetainflem4 27647
Description: Lemma for noeta 27650. If 𝐴 precedes 𝐡, then π‘Š is greater than 𝐴. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypotheses
Ref Expression
noetainflem.1 𝑇 = if(βˆƒπ‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯, ((β„©π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯) βˆͺ {⟨dom (β„©π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯), 1o⟩}), (𝑔 ∈ {𝑦 ∣ βˆƒπ‘’ ∈ 𝐡 (𝑦 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐡 (Β¬ 𝑒 <s 𝑣 β†’ (𝑒 β†Ύ suc 𝑦) = (𝑣 β†Ύ suc 𝑦)))} ↦ (β„©π‘₯βˆƒπ‘’ ∈ 𝐡 (𝑔 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐡 (Β¬ 𝑒 <s 𝑣 β†’ (𝑒 β†Ύ suc 𝑔) = (𝑣 β†Ύ suc 𝑔)) ∧ (π‘’β€˜π‘”) = π‘₯))))
noetainflem.2 π‘Š = (𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))
Assertion
Ref Expression
noetainflem4 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V) ∧ βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏) β†’ βˆ€π‘Ž ∈ 𝐴 π‘Ž <s π‘Š)
Distinct variable groups:   𝐡,𝑔,𝑒,𝑣,π‘₯,𝑦   𝐴,π‘Ž   π‘Ž,𝑏,𝑔,π‘₯,𝐡   𝑣,𝑏,π‘₯,𝑦   𝑇,𝑏,𝑔
Allowed substitution hints:   𝐴(π‘₯,𝑦,𝑣,𝑒,𝑔,𝑏)   𝑇(π‘₯,𝑦,𝑣,𝑒,π‘Ž)   π‘Š(π‘₯,𝑦,𝑣,𝑒,𝑔,π‘Ž,𝑏)
Proof of Theorem noetainflem4
Dummy variables 𝑝 π‘ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplrl 776 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ 𝐡 βŠ† No )
2 simplrr 777 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ 𝐡 ∈ V)
3 simpll 766 . . . . . 6 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) β†’ 𝐴 βŠ† No )
43sselda 3978 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ No )
5 noetainflem.1 . . . . . 6 𝑇 = if(βˆƒπ‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯, ((β„©π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯) βˆͺ {⟨dom (β„©π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 <s π‘₯), 1o⟩}), (𝑔 ∈ {𝑦 ∣ βˆƒπ‘’ ∈ 𝐡 (𝑦 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐡 (Β¬ 𝑒 <s 𝑣 β†’ (𝑒 β†Ύ suc 𝑦) = (𝑣 β†Ύ suc 𝑦)))} ↦ (β„©π‘₯βˆƒπ‘’ ∈ 𝐡 (𝑔 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐡 (Β¬ 𝑒 <s 𝑣 β†’ (𝑒 β†Ύ suc 𝑔) = (𝑣 β†Ύ suc 𝑔)) ∧ (π‘’β€˜π‘”) = π‘₯))))
65noinfbnd2 27638 . . . . 5 ((𝐡 βŠ† No ∧ 𝐡 ∈ V ∧ π‘Ž ∈ No ) β†’ (βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 ↔ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇)))
71, 2, 4, 6syl3anc 1369 . . . 4 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ (βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 ↔ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇)))
8 simplll 774 . . . . . . . . . . 11 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ 𝐴 βŠ† No )
9 simprl 770 . . . . . . . . . . 11 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ π‘Ž ∈ 𝐴)
108, 9sseldd 3979 . . . . . . . . . 10 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ π‘Ž ∈ No )
11 nodmord 27560 . . . . . . . . . 10 (π‘Ž ∈ No β†’ Ord dom π‘Ž)
12 ordirr 6381 . . . . . . . . . 10 (Ord dom π‘Ž β†’ Β¬ dom π‘Ž ∈ dom π‘Ž)
1310, 11, 123syl 18 . . . . . . . . 9 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ Β¬ dom π‘Ž ∈ dom π‘Ž)
14 bdayval 27555 . . . . . . . . . . . . . . 15 (π‘Ž ∈ No β†’ ( bday β€˜π‘Ž) = dom π‘Ž)
1510, 14syl 17 . . . . . . . . . . . . . 14 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ ( bday β€˜π‘Ž) = dom π‘Ž)
16 bdayfo 27584 . . . . . . . . . . . . . . . 16 bday : No –ontoβ†’On
17 fofn 6807 . . . . . . . . . . . . . . . 16 ( bday : No –ontoβ†’On β†’ bday Fn No )
1816, 17ax-mp 5 . . . . . . . . . . . . . . 15 bday Fn No
19 fnfvima 7239 . . . . . . . . . . . . . . 15 (( bday Fn No ∧ 𝐴 βŠ† No ∧ π‘Ž ∈ 𝐴) β†’ ( bday β€˜π‘Ž) ∈ ( bday β€œ 𝐴))
2018, 8, 9, 19mp3an2i 1463 . . . . . . . . . . . . . 14 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ ( bday β€˜π‘Ž) ∈ ( bday β€œ 𝐴))
2115, 20eqeltrrd 2829 . . . . . . . . . . . . 13 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ dom π‘Ž ∈ ( bday β€œ 𝐴))
22 elssuni 4935 . . . . . . . . . . . . 13 (dom π‘Ž ∈ ( bday β€œ 𝐴) β†’ dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴))
2321, 22syl 17 . . . . . . . . . . . 12 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴))
24 nodmon 27557 . . . . . . . . . . . . 13 (π‘Ž ∈ No β†’ dom π‘Ž ∈ On)
25 imassrn 6068 . . . . . . . . . . . . . . . 16 ( bday β€œ 𝐴) βŠ† ran bday
26 forn 6808 . . . . . . . . . . . . . . . . 17 ( bday : No –ontoβ†’On β†’ ran bday = On)
2716, 26ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
2825, 27sseqtri 4014 . . . . . . . . . . . . . . 15 ( bday β€œ 𝐴) βŠ† On
29 ssorduni 7773 . . . . . . . . . . . . . . 15 (( bday β€œ 𝐴) βŠ† On β†’ Ord βˆͺ ( bday β€œ 𝐴))
3028, 29ax-mp 5 . . . . . . . . . . . . . 14 Ord βˆͺ ( bday β€œ 𝐴)
31 ordsssuc 6452 . . . . . . . . . . . . . 14 ((dom π‘Ž ∈ On ∧ Ord βˆͺ ( bday β€œ 𝐴)) β†’ (dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴) ↔ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)))
3230, 31mpan2 690 . . . . . . . . . . . . 13 (dom π‘Ž ∈ On β†’ (dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴) ↔ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)))
3310, 24, 323syl 18 . . . . . . . . . . . 12 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ (dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴) ↔ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)))
3423, 33mpbid 231 . . . . . . . . . . 11 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴))
35 elun2 4173 . . . . . . . . . . 11 (dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴) β†’ dom π‘Ž ∈ (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)))
3634, 35syl 17 . . . . . . . . . 10 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ dom π‘Ž ∈ (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)))
37 eleq2 2817 . . . . . . . . . 10 (dom π‘Ž = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)) β†’ (dom π‘Ž ∈ dom π‘Ž ↔ dom π‘Ž ∈ (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴))))
3836, 37syl5ibrcom 246 . . . . . . . . 9 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ (dom π‘Ž = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)) β†’ dom π‘Ž ∈ dom π‘Ž))
3913, 38mtod 197 . . . . . . . 8 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ Β¬ dom π‘Ž = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)))
40 dmeq 5900 . . . . . . . . 9 (π‘Ž = π‘Š β†’ dom π‘Ž = dom π‘Š)
41 noetainflem.2 . . . . . . . . . . 11 π‘Š = (𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))
4241dmeqi 5901 . . . . . . . . . 10 dom π‘Š = dom (𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))
43 dmun 5907 . . . . . . . . . 10 dom (𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})) = (dom 𝑇 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))
44 2oex 8489 . . . . . . . . . . . . . 14 2o ∈ V
4544snnz 4776 . . . . . . . . . . . . 13 {2o} β‰  βˆ…
46 dmxp 5925 . . . . . . . . . . . . 13 ({2o} β‰  βˆ… β†’ dom ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}) = (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇))
4745, 46ax-mp 5 . . . . . . . . . . . 12 dom ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}) = (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇)
4847uneq2i 4156 . . . . . . . . . . 11 (dom 𝑇 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})) = (dom 𝑇 βˆͺ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇))
49 undif2 4472 . . . . . . . . . . 11 (dom 𝑇 βˆͺ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇)) = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴))
5048, 49eqtri 2755 . . . . . . . . . 10 (dom 𝑇 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})) = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴))
5142, 43, 503eqtri 2759 . . . . . . . . 9 dom π‘Š = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴))
5240, 51eqtrdi 2783 . . . . . . . 8 (π‘Ž = π‘Š β†’ dom π‘Ž = (dom 𝑇 βˆͺ suc βˆͺ ( bday β€œ 𝐴)))
5339, 52nsyl 140 . . . . . . 7 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ Β¬ π‘Ž = π‘Š)
5453neqned 2942 . . . . . 6 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ π‘Ž β‰  π‘Š)
55 simpr 484 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇)
5610adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ π‘Ž ∈ No )
5756adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ π‘Ž ∈ No )
58 simp-4r 783 . . . . . . . . . . . . . . . . . 18 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ 𝐴 ∈ V)
59 simplrl 776 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ 𝐡 βŠ† No )
6059adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ 𝐡 βŠ† No )
61 simplrr 777 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ 𝐡 ∈ V)
6261adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ 𝐡 ∈ V)
635, 41noetainflem1 27644 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ 𝐡 βŠ† No ∧ 𝐡 ∈ V) β†’ π‘Š ∈ No )
6458, 60, 62, 63syl3anc 1369 . . . . . . . . . . . . . . . . 17 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ π‘Š ∈ No )
6564adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ π‘Š ∈ No )
66 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ π‘Ž β‰  π‘Š)
67 nosepne 27587 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ No ∧ π‘Š ∈ No ∧ π‘Ž β‰  π‘Š) β†’ (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
6857, 65, 66, 67syl3anc 1369 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
6955fvresd 6911 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((π‘Š β†Ύ dom 𝑇)β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
70 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝐡 βŠ† No ∧ 𝐡 ∈ V))
715, 41noetainflem2 27645 . . . . . . . . . . . . . . . . . 18 ((𝐡 βŠ† No ∧ 𝐡 ∈ V) β†’ (π‘Š β†Ύ dom 𝑇) = 𝑇)
7270, 71syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘Š β†Ύ dom 𝑇) = 𝑇)
7372fveq1d 6893 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((π‘Š β†Ύ dom 𝑇)β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
7469, 73eqtr3d 2769 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
7568, 74neeqtrd 3005 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
7675necomd 2991 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
77 fveq2 6891 . . . . . . . . . . . . . . 15 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} β†’ (π‘‡β€˜π‘ž) = (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
78 fveq2 6891 . . . . . . . . . . . . . . 15 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} β†’ (π‘Žβ€˜π‘ž) = (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
7977, 78neeq12d 2997 . . . . . . . . . . . . . 14 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} β†’ ((π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž) ↔ (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)})))
8079rspcev 3607 . . . . . . . . . . . . 13 ((∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇 ∧ (π‘‡β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β‰  (π‘Žβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)})) β†’ βˆƒπ‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž))
8155, 76, 80syl2anc 583 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ βˆƒπ‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž))
82 df-ne 2936 . . . . . . . . . . . . . . 15 ((π‘‡β€˜π‘ž) β‰  ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) ↔ Β¬ (π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))
83 fvres 6910 . . . . . . . . . . . . . . . 16 (π‘ž ∈ dom 𝑇 β†’ ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) = (π‘Žβ€˜π‘ž))
8483neeq2d 2996 . . . . . . . . . . . . . . 15 (π‘ž ∈ dom 𝑇 β†’ ((π‘‡β€˜π‘ž) β‰  ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) ↔ (π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž)))
8582, 84bitr3id 285 . . . . . . . . . . . . . 14 (π‘ž ∈ dom 𝑇 β†’ (Β¬ (π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) ↔ (π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž)))
8685rexbiia 3087 . . . . . . . . . . . . 13 (βˆƒπ‘ž ∈ dom 𝑇 Β¬ (π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) ↔ βˆƒπ‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž))
87 rexnal 3095 . . . . . . . . . . . . 13 (βˆƒπ‘ž ∈ dom 𝑇 Β¬ (π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž) ↔ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))
8886, 87bitr3i 277 . . . . . . . . . . . 12 (βˆƒπ‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) β‰  (π‘Žβ€˜π‘ž) ↔ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))
8981, 88sylib 217 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))
9089olcd 873 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (Β¬ dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∨ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)))
915noinfno 27625 . . . . . . . . . . . . . . . 16 ((𝐡 βŠ† No ∧ 𝐡 ∈ V) β†’ 𝑇 ∈ No )
9291ad3antlr 730 . . . . . . . . . . . . . . 15 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ 𝑇 ∈ No )
9392adantr 480 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ 𝑇 ∈ No )
94 nofun 27556 . . . . . . . . . . . . . 14 (𝑇 ∈ No β†’ Fun 𝑇)
9593, 94syl 17 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ Fun 𝑇)
96 nofun 27556 . . . . . . . . . . . . . 14 (π‘Ž ∈ No β†’ Fun π‘Ž)
97 funres 6589 . . . . . . . . . . . . . 14 (Fun π‘Ž β†’ Fun (π‘Ž β†Ύ dom 𝑇))
9857, 96, 973syl 18 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ Fun (π‘Ž β†Ύ dom 𝑇))
99 eqfunfv 7039 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ Fun (π‘Ž β†Ύ dom 𝑇)) β†’ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ↔ (dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∧ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))))
10095, 98, 99syl2anc 583 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ↔ (dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∧ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))))
101 ianor 980 . . . . . . . . . . . . 13 (Β¬ (dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∧ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)) ↔ (Β¬ dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∨ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)))
102101con1bii 356 . . . . . . . . . . . 12 (Β¬ (Β¬ dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∨ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)) ↔ (dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∧ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)))
103100, 102bitr4di 289 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ↔ Β¬ (Β¬ dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∨ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž))))
104103con2bid 354 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((Β¬ dom 𝑇 = dom (π‘Ž β†Ύ dom 𝑇) ∨ Β¬ βˆ€π‘ž ∈ dom 𝑇(π‘‡β€˜π‘ž) = ((π‘Ž β†Ύ dom 𝑇)β€˜π‘ž)) ↔ Β¬ 𝑇 = (π‘Ž β†Ύ dom 𝑇)))
10590, 104mpbid 231 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ Β¬ 𝑇 = (π‘Ž β†Ύ dom 𝑇))
106105pm2.21d 121 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝑇 = (π‘Ž β†Ύ dom 𝑇) β†’ π‘Ž <s π‘Š))
10772breq2d 5154 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((π‘Ž β†Ύ dom 𝑇) <s (π‘Š β†Ύ dom 𝑇) ↔ (π‘Ž β†Ύ dom 𝑇) <s 𝑇))
108 nodmon 27557 . . . . . . . . . . . 12 (𝑇 ∈ No β†’ dom 𝑇 ∈ On)
10992, 108syl 17 . . . . . . . . . . 11 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ dom 𝑇 ∈ On)
110109adantr 480 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ dom 𝑇 ∈ On)
111 sltres 27569 . . . . . . . . . 10 ((π‘Ž ∈ No ∧ π‘Š ∈ No ∧ dom 𝑇 ∈ On) β†’ ((π‘Ž β†Ύ dom 𝑇) <s (π‘Š β†Ύ dom 𝑇) β†’ π‘Ž <s π‘Š))
11257, 65, 110, 111syl3anc 1369 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((π‘Ž β†Ύ dom 𝑇) <s (π‘Š β†Ύ dom 𝑇) β†’ π‘Ž <s π‘Š))
113107, 112sylbird 260 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((π‘Ž β†Ύ dom 𝑇) <s 𝑇 β†’ π‘Ž <s π‘Š))
114 simplrr 777 . . . . . . . . . 10 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))
115114adantr 480 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))
116 noreson 27567 . . . . . . . . . . . . 13 ((π‘Ž ∈ No ∧ dom 𝑇 ∈ On) β†’ (π‘Ž β†Ύ dom 𝑇) ∈ No )
11756, 109, 116syl2anc 583 . . . . . . . . . . . 12 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ (π‘Ž β†Ύ dom 𝑇) ∈ No )
118117adantr 480 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (π‘Ž β†Ύ dom 𝑇) ∈ No )
119 sltso 27583 . . . . . . . . . . . 12 <s Or No
120 sotric 5612 . . . . . . . . . . . 12 (( <s Or No ∧ (𝑇 ∈ No ∧ (π‘Ž β†Ύ dom 𝑇) ∈ No )) β†’ (𝑇 <s (π‘Ž β†Ύ dom 𝑇) ↔ Β¬ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ∨ (π‘Ž β†Ύ dom 𝑇) <s 𝑇)))
121119, 120mpan 689 . . . . . . . . . . 11 ((𝑇 ∈ No ∧ (π‘Ž β†Ύ dom 𝑇) ∈ No ) β†’ (𝑇 <s (π‘Ž β†Ύ dom 𝑇) ↔ Β¬ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ∨ (π‘Ž β†Ύ dom 𝑇) <s 𝑇)))
12293, 118, 121syl2anc 583 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝑇 <s (π‘Ž β†Ύ dom 𝑇) ↔ Β¬ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ∨ (π‘Ž β†Ύ dom 𝑇) <s 𝑇)))
123122con2bid 354 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ ((𝑇 = (π‘Ž β†Ύ dom 𝑇) ∨ (π‘Ž β†Ύ dom 𝑇) <s 𝑇) ↔ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇)))
124115, 123mpbird 257 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ (𝑇 = (π‘Ž β†Ύ dom 𝑇) ∨ (π‘Ž β†Ύ dom 𝑇) <s 𝑇))
125106, 113, 124mpjaod 859 . . . . . . 7 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇) β†’ π‘Ž <s π‘Š)
12664adantr 480 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Š ∈ No )
12756adantr 480 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Ž ∈ No )
128 simplr 768 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Ž β‰  π‘Š)
129128necomd 2991 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Š β‰  π‘Ž)
13041fveq1i 6892 . . . . . . . . 9 (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = ((𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)})
13192adantr 480 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ 𝑇 ∈ No )
132131, 94syl 17 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ Fun 𝑇)
133132funfnd 6578 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ 𝑇 Fn dom 𝑇)
134 fnconstg 6779 . . . . . . . . . . . . 13 (2o ∈ V β†’ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}) Fn (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇))
13544, 134ax-mp 5 . . . . . . . . . . . 12 ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}) Fn (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇)
136135a1i 11 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}) Fn (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇))
137 disjdif 4467 . . . . . . . . . . . 12 (dom 𝑇 ∩ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇)) = βˆ…
138137a1i 11 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ (dom 𝑇 ∩ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇)) = βˆ…)
139 nosepssdm 27593 . . . . . . . . . . . . . 14 ((π‘Ž ∈ No ∧ π‘Š ∈ No ∧ π‘Ž β‰  π‘Š) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} βŠ† dom π‘Ž)
140127, 126, 128, 139syl3anc 1369 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} βŠ† dom π‘Ž)
141127, 14syl 17 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ( bday β€˜π‘Ž) = dom π‘Ž)
142 simp-5l 784 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ 𝐴 βŠ† No )
143 simplrl 776 . . . . . . . . . . . . . . . . . 18 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ π‘Ž ∈ 𝐴)
144143adantr 480 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Ž ∈ 𝐴)
14518, 142, 144, 19mp3an2i 1463 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ( bday β€˜π‘Ž) ∈ ( bday β€œ 𝐴))
146 elssuni 4935 . . . . . . . . . . . . . . . 16 (( bday β€˜π‘Ž) ∈ ( bday β€œ 𝐴) β†’ ( bday β€˜π‘Ž) βŠ† βˆͺ ( bday β€œ 𝐴))
147145, 146syl 17 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ( bday β€˜π‘Ž) βŠ† βˆͺ ( bday β€œ 𝐴))
148141, 147eqsstrrd 4017 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴))
149127, 24, 323syl 18 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ (dom π‘Ž βŠ† βˆͺ ( bday β€œ 𝐴) ↔ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)))
150148, 149mpbid 231 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴))
151 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ π‘Ž β‰  π‘Š)
152 nosepon 27572 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ No ∧ π‘Š ∈ No ∧ π‘Ž β‰  π‘Š) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ On)
15356, 64, 151, 152syl3anc 1369 . . . . . . . . . . . . . . 15 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ On)
154153adantr 480 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ On)
155 eloni 6373 . . . . . . . . . . . . . 14 (∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ On β†’ Ord ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)})
156 ordsuc 7808 . . . . . . . . . . . . . . . 16 (Ord βˆͺ ( bday β€œ 𝐴) ↔ Ord suc βˆͺ ( bday β€œ 𝐴))
15730, 156mpbi 229 . . . . . . . . . . . . . . 15 Ord suc βˆͺ ( bday β€œ 𝐴)
158 ordtr2 6407 . . . . . . . . . . . . . . 15 ((Ord ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∧ Ord suc βˆͺ ( bday β€œ 𝐴)) β†’ ((∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} βŠ† dom π‘Ž ∧ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐴)))
159157, 158mpan2 690 . . . . . . . . . . . . . 14 (Ord ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} β†’ ((∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} βŠ† dom π‘Ž ∧ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐴)))
160154, 155, 1593syl 18 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ((∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} βŠ† dom π‘Ž ∧ dom π‘Ž ∈ suc βˆͺ ( bday β€œ 𝐴)) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐴)))
161140, 150, 160mp2and 698 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐴))
162 ontri1 6397 . . . . . . . . . . . . . 14 ((dom 𝑇 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ On) β†’ (dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ↔ Β¬ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇))
163109, 153, 162syl2anc 583 . . . . . . . . . . . . 13 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ (dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ↔ Β¬ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇))
164163biimpa 476 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ Β¬ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇)
165161, 164eldifd 3955 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇))
166133, 136, 138, 165fvun2d 6986 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ((𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = (((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
16744fvconst2 7210 . . . . . . . . . . 11 (∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ (suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) β†’ (((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = 2o)
168165, 167syl 17 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ (((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = 2o)
169166, 168eqtrd 2767 . . . . . . . . 9 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ ((𝑇 βˆͺ ((suc βˆͺ ( bday β€œ 𝐴) βˆ– dom 𝑇) Γ— {2o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = 2o)
170130, 169eqtrid 2779 . . . . . . . 8 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = 2o)
171 nosep2o 27589 . . . . . . . 8 (((π‘Š ∈ No ∧ π‘Ž ∈ No ∧ π‘Š β‰  π‘Ž) ∧ (π‘Šβ€˜βˆ© {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) = 2o) β†’ π‘Ž <s π‘Š)
172126, 127, 129, 170, 171syl31anc 1371 . . . . . . 7 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) ∧ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}) β†’ π‘Ž <s π‘Š)
173153, 155syl 17 . . . . . . . 8 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ Ord ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)})
174 nodmord 27560 . . . . . . . . 9 (𝑇 ∈ No β†’ Ord dom 𝑇)
17592, 174syl 17 . . . . . . . 8 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ Ord dom 𝑇)
176 ordtri2or 6461 . . . . . . . 8 ((Ord ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∧ Ord dom 𝑇) β†’ (∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇 ∨ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
177173, 175, 176syl2anc 583 . . . . . . 7 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ (∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)} ∈ dom 𝑇 ∨ dom 𝑇 βŠ† ∩ {𝑝 ∈ On ∣ (π‘Žβ€˜π‘) β‰  (π‘Šβ€˜π‘)}))
178125, 172, 177mpjaodan 957 . . . . . 6 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) ∧ π‘Ž β‰  π‘Š) β†’ π‘Ž <s π‘Š)
17954, 178mpdan 686 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (π‘Ž ∈ 𝐴 ∧ Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇))) β†’ π‘Ž <s π‘Š)
180179expr 456 . . . 4 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ (Β¬ 𝑇 <s (π‘Ž β†Ύ dom 𝑇) β†’ π‘Ž <s π‘Š))
1817, 180sylbid 239 . . 3 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ π‘Ž ∈ 𝐴) β†’ (βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 β†’ π‘Ž <s π‘Š))
182181ralimdva 3162 . 2 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) β†’ (βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 β†’ βˆ€π‘Ž ∈ 𝐴 π‘Ž <s π‘Š))
1831823impia 1115 1 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V) ∧ βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏) β†’ βˆ€π‘Ž ∈ 𝐴 π‘Ž <s π‘Š)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 846   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  {cab 2704   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427  Vcvv 3469   βˆ– cdif 3941   βˆͺ cun 3942   ∩ cin 3943   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524  {csn 4624  βŸ¨cop 4630  βˆͺ cuni 4903  βˆ© cint 4944   class class class wbr 5142   ↦ cmpt 5225   Or wor 5583   Γ— cxp 5670  dom cdm 5672  ran crn 5673   β†Ύ cres 5674   β€œ cima 5675  Ord word 6362  Oncon0 6363  suc csuc 6365  β„©cio 6492  Fun wfun 6536   Fn wfn 6537  β€“ontoβ†’wfo 6540  β€˜cfv 6542  β„©crio 7369  1oc1o 8471  2oc2o 8472   No csur 27547   <s cslt 27548   bday cbday 27549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-1o 8478  df-2o 8479  df-no 27550  df-slt 27551  df-bday 27552
This theorem is referenced by:  noetalem1  27648
  Copyright terms: Public domain W3C validator