MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noetasuplem4 Structured version   Visualization version   GIF version

Theorem noetasuplem4 27100
Description: Lemma for noeta 27107. When 𝐴 and 𝐡 are separated, then 𝑍 is a lower bound for 𝐡. Part of Theorem 5.1 of [Lipparini] p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021.)
Hypotheses
Ref Expression
noetasuplem.1 𝑆 = if(βˆƒπ‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦, ((β„©π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦) βˆͺ {⟨dom (β„©π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ βˆƒπ‘’ ∈ 𝐴 (𝑦 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐴 (Β¬ 𝑣 <s 𝑒 β†’ (𝑒 β†Ύ suc 𝑦) = (𝑣 β†Ύ suc 𝑦)))} ↦ (β„©π‘₯βˆƒπ‘’ ∈ 𝐴 (𝑔 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐴 (Β¬ 𝑣 <s 𝑒 β†’ (𝑒 β†Ύ suc 𝑔) = (𝑣 β†Ύ suc 𝑔)) ∧ (π‘’β€˜π‘”) = π‘₯))))
noetasuplem.2 𝑍 = (𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))
Assertion
Ref Expression
noetasuplem4 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V) ∧ βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏) β†’ βˆ€π‘ ∈ 𝐡 𝑍 <s 𝑏)
Distinct variable groups:   𝐴,π‘Ž,𝑏,𝑔   𝑒,π‘Ž,𝐴,𝑣,π‘₯,𝑦   𝐡,π‘Ž,𝑏   𝑔,𝑏,π‘₯   𝑒,𝑔,𝑣,π‘₯,𝑦   𝑆,π‘Ž,𝑔   𝑣,𝑒,π‘₯,𝑦
Allowed substitution hints:   𝐡(π‘₯,𝑦,𝑣,𝑒,𝑔)   𝑆(π‘₯,𝑦,𝑣,𝑒,𝑏)   𝑍(π‘₯,𝑦,𝑣,𝑒,𝑔,π‘Ž,𝑏)

Proof of Theorem noetasuplem4
Dummy variables 𝑝 π‘ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralcom 3271 . . 3 (βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 ↔ βˆ€π‘ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐴 π‘Ž <s 𝑏)
2 simplll 774 . . . . . 6 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ 𝐴 βŠ† No )
3 simpllr 775 . . . . . 6 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ 𝐴 ∈ V)
4 simprl 770 . . . . . . 7 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) β†’ 𝐡 βŠ† No )
54sselda 3945 . . . . . 6 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ 𝑏 ∈ No )
6 noetasuplem.1 . . . . . . 7 𝑆 = if(βˆƒπ‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦, ((β„©π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦) βˆͺ {⟨dom (β„©π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ βˆƒπ‘’ ∈ 𝐴 (𝑦 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐴 (Β¬ 𝑣 <s 𝑒 β†’ (𝑒 β†Ύ suc 𝑦) = (𝑣 β†Ύ suc 𝑦)))} ↦ (β„©π‘₯βˆƒπ‘’ ∈ 𝐴 (𝑔 ∈ dom 𝑒 ∧ βˆ€π‘£ ∈ 𝐴 (Β¬ 𝑣 <s 𝑒 β†’ (𝑒 β†Ύ suc 𝑔) = (𝑣 β†Ύ suc 𝑔)) ∧ (π‘’β€˜π‘”) = π‘₯))))
76nosupbnd2 27080 . . . . . 6 ((𝐴 βŠ† No ∧ 𝐴 ∈ V ∧ 𝑏 ∈ No ) β†’ (βˆ€π‘Ž ∈ 𝐴 π‘Ž <s 𝑏 ↔ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆))
82, 3, 5, 7syl3anc 1372 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ (βˆ€π‘Ž ∈ 𝐴 π‘Ž <s 𝑏 ↔ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆))
9 simpl 484 . . . . . . . . . . 11 ((𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆) β†’ 𝑏 ∈ 𝐡)
10 ssel2 3940 . . . . . . . . . . 11 ((𝐡 βŠ† No ∧ 𝑏 ∈ 𝐡) β†’ 𝑏 ∈ No )
114, 9, 10syl2an 597 . . . . . . . . . 10 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ 𝑏 ∈ No )
12 nodmord 27017 . . . . . . . . . 10 (𝑏 ∈ No β†’ Ord dom 𝑏)
13 ordirr 6336 . . . . . . . . . 10 (Ord dom 𝑏 β†’ Β¬ dom 𝑏 ∈ dom 𝑏)
1411, 12, 133syl 18 . . . . . . . . 9 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ Β¬ dom 𝑏 ∈ dom 𝑏)
15 ssun2 4134 . . . . . . . . . . 11 suc βˆͺ ( bday β€œ 𝐡) βŠ† (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡))
16 bdayval 27012 . . . . . . . . . . . . . . 15 (𝑏 ∈ No β†’ ( bday β€˜π‘) = dom 𝑏)
1711, 16syl 17 . . . . . . . . . . . . . 14 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ ( bday β€˜π‘) = dom 𝑏)
18 bdayfo 27041 . . . . . . . . . . . . . . . . 17 bday : No –ontoβ†’On
19 fofn 6759 . . . . . . . . . . . . . . . . 17 ( bday : No –ontoβ†’On β†’ bday Fn No )
2018, 19ax-mp 5 . . . . . . . . . . . . . . . 16 bday Fn No
21 fnfvima 7184 . . . . . . . . . . . . . . . 16 (( bday Fn No ∧ 𝐡 βŠ† No ∧ 𝑏 ∈ 𝐡) β†’ ( bday β€˜π‘) ∈ ( bday β€œ 𝐡))
2220, 21mp3an1 1449 . . . . . . . . . . . . . . 15 ((𝐡 βŠ† No ∧ 𝑏 ∈ 𝐡) β†’ ( bday β€˜π‘) ∈ ( bday β€œ 𝐡))
234, 9, 22syl2an 597 . . . . . . . . . . . . . 14 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ ( bday β€˜π‘) ∈ ( bday β€œ 𝐡))
2417, 23eqeltrrd 2835 . . . . . . . . . . . . 13 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ dom 𝑏 ∈ ( bday β€œ 𝐡))
25 elssuni 4899 . . . . . . . . . . . . 13 (dom 𝑏 ∈ ( bday β€œ 𝐡) β†’ dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡))
2624, 25syl 17 . . . . . . . . . . . 12 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡))
27 nodmon 27014 . . . . . . . . . . . . 13 (𝑏 ∈ No β†’ dom 𝑏 ∈ On)
28 imassrn 6025 . . . . . . . . . . . . . . . 16 ( bday β€œ 𝐡) βŠ† ran bday
29 forn 6760 . . . . . . . . . . . . . . . . 17 ( bday : No –ontoβ†’On β†’ ran bday = On)
3018, 29ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
3128, 30sseqtri 3981 . . . . . . . . . . . . . . 15 ( bday β€œ 𝐡) βŠ† On
32 ssorduni 7714 . . . . . . . . . . . . . . 15 (( bday β€œ 𝐡) βŠ† On β†’ Ord βˆͺ ( bday β€œ 𝐡))
3331, 32ax-mp 5 . . . . . . . . . . . . . 14 Ord βˆͺ ( bday β€œ 𝐡)
34 ordsssuc 6407 . . . . . . . . . . . . . 14 ((dom 𝑏 ∈ On ∧ Ord βˆͺ ( bday β€œ 𝐡)) β†’ (dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡) ↔ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)))
3533, 34mpan2 690 . . . . . . . . . . . . 13 (dom 𝑏 ∈ On β†’ (dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡) ↔ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)))
3611, 27, 353syl 18 . . . . . . . . . . . 12 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ (dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡) ↔ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)))
3726, 36mpbid 231 . . . . . . . . . . 11 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡))
3815, 37sselid 3943 . . . . . . . . . 10 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ dom 𝑏 ∈ (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)))
39 eleq2 2823 . . . . . . . . . 10 ((dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)) = dom 𝑏 β†’ (dom 𝑏 ∈ (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)) ↔ dom 𝑏 ∈ dom 𝑏))
4038, 39syl5ibcom 244 . . . . . . . . 9 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ ((dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)) = dom 𝑏 β†’ dom 𝑏 ∈ dom 𝑏))
4114, 40mtod 197 . . . . . . . 8 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ Β¬ (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)) = dom 𝑏)
42 noetasuplem.2 . . . . . . . . . . . 12 𝑍 = (𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))
4342dmeqi 5861 . . . . . . . . . . 11 dom 𝑍 = dom (𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))
44 dmun 5867 . . . . . . . . . . 11 dom (𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})) = (dom 𝑆 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))
4543, 44eqtri 2761 . . . . . . . . . 10 dom 𝑍 = (dom 𝑆 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))
46 1oex 8423 . . . . . . . . . . . . 13 1o ∈ V
4746snnz 4738 . . . . . . . . . . . 12 {1o} β‰  βˆ…
48 dmxp 5885 . . . . . . . . . . . 12 ({1o} β‰  βˆ… β†’ dom ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) = (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))
4947, 48ax-mp 5 . . . . . . . . . . 11 dom ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) = (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)
5049uneq2i 4121 . . . . . . . . . 10 (dom 𝑆 βˆͺ dom ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})) = (dom 𝑆 βˆͺ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))
51 undif2 4437 . . . . . . . . . 10 (dom 𝑆 βˆͺ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)) = (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡))
5245, 50, 513eqtri 2765 . . . . . . . . 9 dom 𝑍 = (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡))
53 dmeq 5860 . . . . . . . . 9 (𝑍 = 𝑏 β†’ dom 𝑍 = dom 𝑏)
5452, 53eqtr3id 2787 . . . . . . . 8 (𝑍 = 𝑏 β†’ (dom 𝑆 βˆͺ suc βˆͺ ( bday β€œ 𝐡)) = dom 𝑏)
5541, 54nsyl 140 . . . . . . 7 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ Β¬ 𝑍 = 𝑏)
56 df-ne 2941 . . . . . . . 8 (𝑍 β‰  𝑏 ↔ Β¬ 𝑍 = 𝑏)
57 notnotr 130 . . . . . . . . . . . . . . 15 (Β¬ Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 β†’ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆)
58 simpr 486 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆)
5958fvresd 6863 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑍 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
6042reseq1i 5934 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 β†Ύ dom 𝑆) = ((𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})) β†Ύ dom 𝑆)
61 resundir 5953 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})) β†Ύ dom 𝑆) = ((𝑆 β†Ύ dom 𝑆) βˆͺ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) β†Ύ dom 𝑆))
62 df-res 5646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) β†Ύ dom 𝑆) = (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) ∩ (dom 𝑆 Γ— V))
63 disjdifr 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) ∩ dom 𝑆) = βˆ…
64 xpdisj1 6114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) ∩ dom 𝑆) = βˆ… β†’ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) ∩ (dom 𝑆 Γ— V)) = βˆ…)
6563, 64ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) ∩ (dom 𝑆 Γ— V)) = βˆ…
6662, 65eqtri 2761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) β†Ύ dom 𝑆) = βˆ…
6766uneq2i 4121 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 β†Ύ dom 𝑆) βˆͺ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) β†Ύ dom 𝑆)) = ((𝑆 β†Ύ dom 𝑆) βˆͺ βˆ…)
68 un0 4351 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 β†Ύ dom 𝑆) βˆͺ βˆ…) = (𝑆 β†Ύ dom 𝑆)
6967, 68eqtri 2761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 β†Ύ dom 𝑆) βˆͺ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) β†Ύ dom 𝑆)) = (𝑆 β†Ύ dom 𝑆)
7060, 61, 693eqtri 2765 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍 β†Ύ dom 𝑆) = (𝑆 β†Ύ dom 𝑆)
71 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ (𝐴 βŠ† No ∧ 𝐴 ∈ V))
726nosupno 27067 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 βŠ† No ∧ 𝐴 ∈ V) β†’ 𝑆 ∈ No )
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑆 ∈ No )
7473adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ 𝑆 ∈ No )
75 nofun 27013 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑆 ∈ No β†’ Fun 𝑆)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ Fun 𝑆)
77 funrel 6519 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑆 β†’ Rel 𝑆)
78 resdm 5983 . . . . . . . . . . . . . . . . . . . . . . . 24 (Rel 𝑆 β†’ (𝑆 β†Ύ dom 𝑆) = 𝑆)
7976, 77, 783syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (𝑆 β†Ύ dom 𝑆) = 𝑆)
8070, 79eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (𝑍 β†Ύ dom 𝑆) = 𝑆)
8180fveq1d 6845 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑍 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
8259, 81eqtr3d 2775 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
83 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝐴 βŠ† No )
84 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝐴 ∈ V)
85 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ 𝐡 ∈ V)
8685adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝐡 ∈ V)
876, 42noetasuplem1 27097 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 βŠ† No ∧ 𝐴 ∈ V ∧ 𝐡 ∈ V) β†’ 𝑍 ∈ No )
8883, 84, 86, 87syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑍 ∈ No )
8988adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ 𝑍 ∈ No )
9011adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑏 ∈ No )
9190adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ 𝑏 ∈ No )
92 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ 𝑍 β‰  𝑏)
93 nosepne 27044 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 β‰  𝑏) β†’ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
9489, 91, 92, 93syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
9582, 94eqnetrrd 3009 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
9658fvresd 6863 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
9795, 96neeqtrrd 3015 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
98 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} β†’ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
99 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} β†’ (π‘†β€˜π‘ž) = (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
10098, 99neeq12d 3002 . . . . . . . . . . . . . . . . . . . 20 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} β†’ (((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) β‰  (π‘†β€˜π‘ž) ↔ ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})))
101 df-ne 2941 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) β‰  (π‘†β€˜π‘ž) ↔ Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))
102 necom 2994 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) ↔ (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
103100, 101, 1023bitr3g 313 . . . . . . . . . . . . . . . . . . 19 (π‘ž = ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} β†’ (Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž) ↔ (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})))
104103rspcev 3580 . . . . . . . . . . . . . . . . . 18 ((∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆 ∧ (π‘†β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β‰  ((𝑏 β†Ύ dom 𝑆)β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})) β†’ βˆƒπ‘ž ∈ dom 𝑆 Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))
10558, 97, 104syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ βˆƒπ‘ž ∈ dom 𝑆 Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))
106 rexeq 3309 . . . . . . . . . . . . . . . . 17 (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 β†’ (βˆƒπ‘ž ∈ dom (𝑏 β†Ύ dom 𝑆) Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž) ↔ βˆƒπ‘ž ∈ dom 𝑆 Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
107105, 106syl5ibrcom 247 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 β†’ βˆƒπ‘ž ∈ dom (𝑏 β†Ύ dom 𝑆) Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
108 rexnal 3100 . . . . . . . . . . . . . . . 16 (βˆƒπ‘ž ∈ dom (𝑏 β†Ύ dom 𝑆) Β¬ ((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž) ↔ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))
109107, 108syl6ib 251 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 β†’ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
11057, 109syl5 34 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (Β¬ Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 β†’ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
111110orrd 862 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∨ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
112 nofun 27013 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ No β†’ Fun 𝑏)
113 funres 6544 . . . . . . . . . . . . . . . . 17 (Fun 𝑏 β†’ Fun (𝑏 β†Ύ dom 𝑆))
11491, 112, 1133syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ Fun (𝑏 β†Ύ dom 𝑆))
115 eqfunfv 6988 . . . . . . . . . . . . . . . 16 ((Fun (𝑏 β†Ύ dom 𝑆) ∧ Fun 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ↔ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∧ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))))
116114, 76, 115syl2anc 585 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ↔ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∧ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))))
117 ianor 981 . . . . . . . . . . . . . . . 16 (Β¬ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∧ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)) ↔ (Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∨ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
118117con1bii 357 . . . . . . . . . . . . . . 15 (Β¬ (Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∨ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)) ↔ (dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∧ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)))
119116, 118bitr4di 289 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ↔ Β¬ (Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∨ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž))))
120119con2bid 355 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((Β¬ dom (𝑏 β†Ύ dom 𝑆) = dom 𝑆 ∨ Β¬ βˆ€π‘ž ∈ dom (𝑏 β†Ύ dom 𝑆)((𝑏 β†Ύ dom 𝑆)β€˜π‘ž) = (π‘†β€˜π‘ž)) ↔ Β¬ (𝑏 β†Ύ dom 𝑆) = 𝑆))
121111, 120mpbid 231 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ Β¬ (𝑏 β†Ύ dom 𝑆) = 𝑆)
122121pm2.21d 121 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) = 𝑆 β†’ 𝑍 <s 𝑏))
12380breq1d 5116 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑍 β†Ύ dom 𝑆) <s (𝑏 β†Ύ dom 𝑆) ↔ 𝑆 <s (𝑏 β†Ύ dom 𝑆)))
124 nodmon 27014 . . . . . . . . . . . . . 14 (𝑆 ∈ No β†’ dom 𝑆 ∈ On)
12574, 124syl 17 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ dom 𝑆 ∈ On)
126 sltres 27026 . . . . . . . . . . . . 13 ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑆 ∈ On) β†’ ((𝑍 β†Ύ dom 𝑆) <s (𝑏 β†Ύ dom 𝑆) β†’ 𝑍 <s 𝑏))
12789, 91, 125, 126syl3anc 1372 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑍 β†Ύ dom 𝑆) <s (𝑏 β†Ύ dom 𝑆) β†’ 𝑍 <s 𝑏))
128123, 127sylbird 260 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (𝑆 <s (𝑏 β†Ύ dom 𝑆) β†’ 𝑍 <s 𝑏))
129 simplrr 777 . . . . . . . . . . . . 13 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)
130129adantr 482 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)
131 noreson 27024 . . . . . . . . . . . . . . 15 ((𝑏 ∈ No ∧ dom 𝑆 ∈ On) β†’ (𝑏 β†Ύ dom 𝑆) ∈ No )
13291, 125, 131syl2anc 585 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (𝑏 β†Ύ dom 𝑆) ∈ No )
133 sltso 27040 . . . . . . . . . . . . . . 15 <s Or No
134 sotric 5574 . . . . . . . . . . . . . . 15 (( <s Or No ∧ ((𝑏 β†Ύ dom 𝑆) ∈ No ∧ 𝑆 ∈ No )) β†’ ((𝑏 β†Ύ dom 𝑆) <s 𝑆 ↔ Β¬ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 β†Ύ dom 𝑆))))
135133, 134mpan 689 . . . . . . . . . . . . . 14 (((𝑏 β†Ύ dom 𝑆) ∈ No ∧ 𝑆 ∈ No ) β†’ ((𝑏 β†Ύ dom 𝑆) <s 𝑆 ↔ Β¬ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 β†Ύ dom 𝑆))))
136132, 74, 135syl2anc 585 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) <s 𝑆 ↔ Β¬ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 β†Ύ dom 𝑆))))
137136con2bid 355 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ (((𝑏 β†Ύ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 β†Ύ dom 𝑆)) ↔ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆))
138130, 137mpbird 257 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ ((𝑏 β†Ύ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑏 β†Ύ dom 𝑆)))
139122, 128, 138mpjaod 859 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆) β†’ 𝑍 <s 𝑏)
14088adantr 482 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑍 ∈ No )
14190adantr 482 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑏 ∈ No )
142 simplr 768 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑍 β‰  𝑏)
14342fveq1i 6844 . . . . . . . . . . . . 13 (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = ((𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})
144 simp-4l 782 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (𝐴 βŠ† No ∧ 𝐴 ∈ V))
145144, 72, 753syl 18 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ Fun 𝑆)
146 funfn 6532 . . . . . . . . . . . . . . 15 (Fun 𝑆 ↔ 𝑆 Fn dom 𝑆)
147145, 146sylib 217 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑆 Fn dom 𝑆)
14846fconst 6729 . . . . . . . . . . . . . . . 16 ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}):(suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)⟢{1o}
149 ffn 6669 . . . . . . . . . . . . . . . 16 (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}):(suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)⟢{1o} β†’ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) Fn (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))
150148, 149ax-mp 5 . . . . . . . . . . . . . . 15 ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) Fn (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)
151150a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) Fn (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))
152 disjdif 4432 . . . . . . . . . . . . . . 15 (dom 𝑆 ∩ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)) = βˆ…
153152a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (dom 𝑆 ∩ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)) = βˆ…)
154 necom 2994 . . . . . . . . . . . . . . . . . . 19 ((π‘β€˜π‘) β‰  (π‘β€˜π‘) ↔ (π‘β€˜π‘) β‰  (π‘β€˜π‘))
155154rabbii 3412 . . . . . . . . . . . . . . . . . 18 {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} = {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}
156155inteqi 4912 . . . . . . . . . . . . . . . . 17 ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} = ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}
157142necomd 2996 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑏 β‰  𝑍)
158 nosepssdm 27050 . . . . . . . . . . . . . . . . . 18 ((𝑏 ∈ No ∧ 𝑍 ∈ No ∧ 𝑏 β‰  𝑍) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏)
159141, 140, 157, 158syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏)
160156, 159eqsstrid 3993 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏)
161141, 16syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ( bday β€˜π‘) = dom 𝑏)
162 simplrl 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ 𝐡 βŠ† No )
163162adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝐡 βŠ† No )
164163adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝐡 βŠ† No )
165 simplrl 776 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑏 ∈ 𝐡)
166165adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑏 ∈ 𝐡)
167164, 166, 22syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ( bday β€˜π‘) ∈ ( bday β€œ 𝐡))
168161, 167eqeltrrd 2835 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ dom 𝑏 ∈ ( bday β€œ 𝐡))
169168, 25syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡))
170141, 27, 353syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (dom 𝑏 βŠ† βˆͺ ( bday β€œ 𝐡) ↔ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)))
171169, 170mpbid 231 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡))
172 nosepon 27029 . . . . . . . . . . . . . . . . . 18 ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 β‰  𝑏) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ On)
173140, 141, 142, 172syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ On)
174 eloni 6328 . . . . . . . . . . . . . . . . 17 (∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ On β†’ Ord ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})
175 ordsuc 7749 . . . . . . . . . . . . . . . . . . 19 (Ord βˆͺ ( bday β€œ 𝐡) ↔ Ord suc βˆͺ ( bday β€œ 𝐡))
17633, 175mpbi 229 . . . . . . . . . . . . . . . . . 18 Ord suc βˆͺ ( bday β€œ 𝐡)
177 ordtr2 6362 . . . . . . . . . . . . . . . . . 18 ((Ord ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∧ Ord suc βˆͺ ( bday β€œ 𝐡)) β†’ ((∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏 ∧ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐡)))
178176, 177mpan2 690 . . . . . . . . . . . . . . . . 17 (Ord ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} β†’ ((∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏 ∧ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐡)))
179173, 174, 1783syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ((∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} βŠ† dom 𝑏 ∧ dom 𝑏 ∈ suc βˆͺ ( bday β€œ 𝐡)) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐡)))
180160, 171, 179mp2and 698 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ suc βˆͺ ( bday β€œ 𝐡))
181 simpr 486 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})
182144, 72, 1243syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ dom 𝑆 ∈ On)
183 ontri1 6352 . . . . . . . . . . . . . . . . 17 ((dom 𝑆 ∈ On ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ On) β†’ (dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ↔ Β¬ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆))
184182, 173, 183syl2anc 585 . . . . . . . . . . . . . . . 16 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ↔ Β¬ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆))
185181, 184mpbid 231 . . . . . . . . . . . . . . 15 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ Β¬ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆)
186180, 185eldifd 3922 . . . . . . . . . . . . . 14 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))
187 fvun2 6934 . . . . . . . . . . . . . 14 ((𝑆 Fn dom 𝑆 ∧ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}) Fn (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) ∧ ((dom 𝑆 ∩ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆)) = βˆ… ∧ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆))) β†’ ((𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
188147, 151, 153, 186, 187syl112anc 1375 . . . . . . . . . . . . 13 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ ((𝑆 βˆͺ ((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o}))β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
189143, 188eqtrid 2785 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
19046fvconst2 7154 . . . . . . . . . . . . 13 (∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ (suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) β†’ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = 1o)
191186, 190syl 17 . . . . . . . . . . . 12 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (((suc βˆͺ ( bday β€œ 𝐡) βˆ– dom 𝑆) Γ— {1o})β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = 1o)
192189, 191eqtrd 2773 . . . . . . . . . . 11 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = 1o)
193 nosep1o 27045 . . . . . . . . . . 11 (((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ 𝑍 β‰  𝑏) ∧ (π‘β€˜βˆ© {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) = 1o) β†’ 𝑍 <s 𝑏)
194140, 141, 142, 192, 193syl31anc 1374 . . . . . . . . . 10 ((((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) ∧ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}) β†’ 𝑍 <s 𝑏)
195 simpr 486 . . . . . . . . . . . . 13 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑍 β‰  𝑏)
19688, 90, 195, 172syl3anc 1372 . . . . . . . . . . . 12 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ On)
197196, 174syl 17 . . . . . . . . . . 11 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ Ord ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)})
198 nodmord 27017 . . . . . . . . . . . 12 (𝑆 ∈ No β†’ Ord dom 𝑆)
19971, 72, 1983syl 18 . . . . . . . . . . 11 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ Ord dom 𝑆)
200 ordtri2or 6416 . . . . . . . . . . 11 ((Ord ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∧ Ord dom 𝑆) β†’ (∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆 ∨ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
201197, 199, 200syl2anc 585 . . . . . . . . . 10 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ (∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)} ∈ dom 𝑆 ∨ dom 𝑆 βŠ† ∩ {𝑝 ∈ On ∣ (π‘β€˜π‘) β‰  (π‘β€˜π‘)}))
202139, 194, 201mpjaodan 958 . . . . . . . . 9 (((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) ∧ 𝑍 β‰  𝑏) β†’ 𝑍 <s 𝑏)
203202ex 414 . . . . . . . 8 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ (𝑍 β‰  𝑏 β†’ 𝑍 <s 𝑏))
20456, 203biimtrrid 242 . . . . . . 7 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ (Β¬ 𝑍 = 𝑏 β†’ 𝑍 <s 𝑏))
20555, 204mpd 15 . . . . . 6 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ (𝑏 ∈ 𝐡 ∧ Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆)) β†’ 𝑍 <s 𝑏)
206205expr 458 . . . . 5 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ (Β¬ (𝑏 β†Ύ dom 𝑆) <s 𝑆 β†’ 𝑍 <s 𝑏))
2078, 206sylbid 239 . . . 4 ((((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) ∧ 𝑏 ∈ 𝐡) β†’ (βˆ€π‘Ž ∈ 𝐴 π‘Ž <s 𝑏 β†’ 𝑍 <s 𝑏))
208207ralimdva 3161 . . 3 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) β†’ (βˆ€π‘ ∈ 𝐡 βˆ€π‘Ž ∈ 𝐴 π‘Ž <s 𝑏 β†’ βˆ€π‘ ∈ 𝐡 𝑍 <s 𝑏))
2091, 208biimtrid 241 . 2 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V)) β†’ (βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏 β†’ βˆ€π‘ ∈ 𝐡 𝑍 <s 𝑏))
2102093impia 1118 1 (((𝐴 βŠ† No ∧ 𝐴 ∈ V) ∧ (𝐡 βŠ† No ∧ 𝐡 ∈ V) ∧ βˆ€π‘Ž ∈ 𝐴 βˆ€π‘ ∈ 𝐡 π‘Ž <s 𝑏) β†’ βˆ€π‘ ∈ 𝐡 𝑍 <s 𝑏)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3444   βˆ– cdif 3908   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  ifcif 4487  {csn 4587  βŸ¨cop 4593  βˆͺ cuni 4866  βˆ© cint 4908   class class class wbr 5106   ↦ cmpt 5189   Or wor 5545   Γ— cxp 5632  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637  Rel wrel 5639  Ord word 6317  Oncon0 6318  suc csuc 6320  β„©cio 6447  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“ontoβ†’wfo 6495  β€˜cfv 6497  β„©crio 7313  1oc1o 8406  2oc2o 8407   No csur 27004   <s cslt 27005   bday cbday 27006
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 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
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 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-1o 8413  df-2o 8414  df-no 27007  df-slt 27008  df-bday 27009
This theorem is referenced by:  noetalem1  27105
  Copyright terms: Public domain W3C validator