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

Theorem noetasuplem4 27795
Description: Lemma for noeta 27802. 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 3286 . . 3 (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 ↔ ∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏)
2 simplll 775 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 No )
3 simpllr 776 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 ∈ V)
4 simprl 771 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐵 No )
54sselda 3994 . . . . . 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 27775 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑏 No ) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
82, 3, 5, 7syl3anc 1370 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9 simpl 482 . . . . . . . . . . 11 ((𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏𝐵)
10 ssel2 3989 . . . . . . . . . . 11 ((𝐵 No 𝑏𝐵) → 𝑏 No )
114, 9, 10syl2an 596 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 No )
12 nodmord 27712 . . . . . . . . . 10 (𝑏 No → Ord dom 𝑏)
13 ordirr 6403 . . . . . . . . . 10 (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
1411, 12, 133syl 18 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15 ssun2 4188 . . . . . . . . . . 11 suc ( bday 𝐵) ⊆ (dom 𝑆 ∪ suc ( bday 𝐵))
16 bdayval 27707 . . . . . . . . . . . . . . 15 (𝑏 No → ( bday 𝑏) = dom 𝑏)
1711, 16syl 17 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) = dom 𝑏)
18 bdayfo 27736 . . . . . . . . . . . . . . . . 17 bday : No onto→On
19 fofn 6822 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → bday Fn No )
2018, 19ax-mp 5 . . . . . . . . . . . . . . . 16 bday Fn No
21 fnfvima 7252 . . . . . . . . . . . . . . . 16 (( bday Fn No 𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
2220, 21mp3an1 1447 . . . . . . . . . . . . . . 15 ((𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
234, 9, 22syl2an 596 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) ∈ ( bday 𝐵))
2417, 23eqeltrrd 2839 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday 𝐵))
25 elssuni 4941 . . . . . . . . . . . . 13 (dom 𝑏 ∈ ( bday 𝐵) → dom 𝑏 ( bday 𝐵))
2624, 25syl 17 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ( bday 𝐵))
27 nodmon 27709 . . . . . . . . . . . . 13 (𝑏 No → dom 𝑏 ∈ On)
28 imassrn 6090 . . . . . . . . . . . . . . . 16 ( bday 𝐵) ⊆ ran bday
29 forn 6823 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → ran bday = On)
3018, 29ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
3128, 30sseqtri 4031 . . . . . . . . . . . . . . 15 ( bday 𝐵) ⊆ On
32 ssorduni 7797 . . . . . . . . . . . . . . 15 (( bday 𝐵) ⊆ On → Ord ( bday 𝐵))
3331, 32ax-mp 5 . . . . . . . . . . . . . 14 Ord ( bday 𝐵)
34 ordsssuc 6474 . . . . . . . . . . . . . 14 ((dom 𝑏 ∈ On ∧ Ord ( bday 𝐵)) → (dom 𝑏 ( bday 𝐵) ↔ dom 𝑏 ∈ suc ( bday 𝐵)))
3533, 34mpan2 691 . . . . . . . . . . . . 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 232 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ( bday 𝐵))
3815, 37sselid 3992 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)))
39 eleq2 2827 . . . . . . . . . 10 ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏))
4038, 39syl5ibcom 245 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏))
4114, 40mtod 198 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
42 noetasuplem.2 . . . . . . . . . . . 12 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
4342dmeqi 5917 . . . . . . . . . . 11 dom 𝑍 = dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
44 dmun 5923 . . . . . . . . . . 11 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
4543, 44eqtri 2762 . . . . . . . . . 10 dom 𝑍 = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
46 1oex 8514 . . . . . . . . . . . . 13 1o ∈ V
4746snnz 4780 . . . . . . . . . . . 12 {1o} ≠ ∅
48 dmxp 5941 . . . . . . . . . . . 12 ({1o} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆))
4947, 48ax-mp 5 . . . . . . . . . . 11 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆)
5049uneq2i 4174 . . . . . . . . . 10 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆))
51 undif2 4482 . . . . . . . . . 10 (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ( bday 𝐵))
5245, 50, 513eqtri 2766 . . . . . . . . 9 dom 𝑍 = (dom 𝑆 ∪ suc ( bday 𝐵))
53 dmeq 5916 . . . . . . . . 9 (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
5452, 53eqtr3id 2788 . . . . . . . 8 (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
5541, 54nsyl 140 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56 df-ne 2938 . . . . . . . 8 (𝑍𝑏 ↔ ¬ 𝑍 = 𝑏)
57 notnotr 130 . . . . . . . . . . . . . . 15 (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆)
58 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
5958fvresd 6926 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
6042reseq1i 5995 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆)
61 resundir 6014 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆))
62 df-res 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V))
63 disjdifr 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
64 xpdisj1 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅)
6563, 64ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅
6662, 65eqtri 2762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅
6766uneq2i 4174 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
68 un0 4399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
6967, 68eqtri 2762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
7060, 61, 693eqtri 2766 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
71 simplll 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → (𝐴 No 𝐴 ∈ V))
726nosupno 27762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑆 No )
7473adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑆 No )
75 nofun 27708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑆 No → Fun 𝑆)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun 𝑆)
77 funrel 6584 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑆 → Rel 𝑆)
78 resdm 6045 . . . . . . . . . . . . . . . . . . . . . . . 24 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
7976, 77, 783syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
8070, 79eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
8180fveq1d 6908 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
8259, 81eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
83 simp-4l 783 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 No )
84 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 ∈ V)
85 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
8685adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 ∈ V)
876, 42noetasuplem1 27792 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
8883, 84, 86, 87syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 No )
8988adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 No )
9011adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏 No )
9190adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑏 No )
92 simplr 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍𝑏)
93 nosepne 27739 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 No 𝑏 No 𝑍𝑏) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9489, 91, 92, 93syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9582, 94eqnetrrd 3006 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9658fvresd 6926 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9795, 96neeqtrrd 3012 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
98 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
99 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (𝑆𝑞) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
10098, 99neeq12d 2999 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
101 df-ne 2938 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
102 necom 2991 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
103100, 101, 1023bitr3g 313 . . . . . . . . . . . . . . . . . . 19 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
104103rspcev 3621 . . . . . . . . . . . . . . . . . 18 (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∧ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
10558, 97, 104syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
106 rexeq 3319 . . . . . . . . . . . . . . . . 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 3097 . . . . . . . . . . . . . . . 16 (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
109107, 108imbitrdi 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 863 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
112 nofun 27708 . . . . . . . . . . . . . . . . 17 (𝑏 No → Fun 𝑏)
113 funres 6609 . . . . . . . . . . . . . . . . 17 (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
11491, 112, 1133syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
115 eqfunfv 7055 . . . . . . . . . . . . . . . 16 ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
116114, 76, 115syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
117 ianor 983 . . . . . . . . . . . . . . . 16 (¬ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
118117con1bii 356 . . . . . . . . . . . . . . 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 354 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆))
121111, 120mpbid 232 . . . . . . . . . . . 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 5157 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
124 nodmon 27709 . . . . . . . . . . . . . 14 (𝑆 No → dom 𝑆 ∈ On)
12574, 124syl 17 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
126 sltres 27721 . . . . . . . . . . . . 13 ((𝑍 No 𝑏 No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
12789, 91, 125, 126syl3anc 1370 . . . . . . . . . . . 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 778 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
130129adantr 480 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
131 noreson 27719 . . . . . . . . . . . . . . 15 ((𝑏 No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
13291, 125, 131syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
133 sltso 27735 . . . . . . . . . . . . . . 15 <s Or No
134 sotric 5625 . . . . . . . . . . . . . . 15 (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
135133, 134mpan 690 . . . . . . . . . . . . . 14 (((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
136132, 74, 135syl2anc 584 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
137136con2bid 354 . . . . . . . . . . . 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 860 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏)
14088adantr 480 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 No )
14190adantr 480 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏 No )
142 simplr 769 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍𝑏)
14342fveq1i 6907 . . . . . . . . . . . . 13 (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
144 simp-4l 783 . . . . . . . . . . . . . . . 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 6597 . . . . . . . . . . . . . . 15 (Fun 𝑆𝑆 Fn dom 𝑆)
147145, 146sylib 218 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑆 Fn dom 𝑆)
14846fconst 6794 . . . . . . . . . . . . . . . 16 ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}):(suc ( bday 𝐵) ∖ dom 𝑆)⟶{1o}
149 ffn 6736 . . . . . . . . . . . . . . . 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 4477 . . . . . . . . . . . . . . 15 (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅
153152a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅)
154 necom 2991 . . . . . . . . . . . . . . . . . . 19 ((𝑍𝑝) ≠ (𝑏𝑝) ↔ (𝑏𝑝) ≠ (𝑍𝑝))
155154rabbii 3438 . . . . . . . . . . . . . . . . . 18 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
156155inteqi 4954 . . . . . . . . . . . . . . . . 17 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
157142necomd 2993 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝑍)
158 nosepssdm 27745 . . . . . . . . . . . . . . . . . 18 ((𝑏 No 𝑍 No 𝑏𝑍) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
159141, 140, 157, 158syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
160156, 159eqsstrid 4043 . . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 No )
163162adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 No )
164163adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝐵 No )
165 simplrl 777 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏𝐵)
166165adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝐵)
167164, 166, 22syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ( bday 𝑏) ∈ ( bday 𝐵))
168161, 167eqeltrrd 2839 . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ∈ suc ( bday 𝐵))
172 nosepon 27724 . . . . . . . . . . . . . . . . . 18 ((𝑍 No 𝑏 No 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
173140, 141, 142, 172syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
174 eloni 6395 . . . . . . . . . . . . . . . . 17 ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
175 ordsuc 7832 . . . . . . . . . . . . . . . . . . 19 (Ord ( bday 𝐵) ↔ Ord suc ( bday 𝐵))
17633, 175mpbi 230 . . . . . . . . . . . . . . . . . 18 Ord suc ( bday 𝐵)
177 ordtr2 6429 . . . . . . . . . . . . . . . . . 18 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord suc ( bday 𝐵)) → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
178176, 177mpan2 691 . . . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵))
181 simpr 484 . . . . . . . . . . . . . . . 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 6419 . . . . . . . . . . . . . . . . 17 ((dom 𝑆 ∈ On ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
184182, 173, 183syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
185181, 184mpbid 232 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
186180, 185eldifd 3973 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆))
187 fvun2 7000 . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
189143, 188eqtrid 2786 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
19046fvconst2 7223 . . . . . . . . . . . . 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 2774 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o)
193 nosep1o 27740 . . . . . . . . . . 11 (((𝑍 No 𝑏 No 𝑍𝑏) ∧ (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o) → 𝑍 <s 𝑏)
194140, 141, 142, 192, 193syl31anc 1372 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 <s 𝑏)
195 simpr 484 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍𝑏)
19688, 90, 195, 172syl3anc 1370 . . . . . . . . . . . 12 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
197196, 174syl 17 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
198 nodmord 27712 . . . . . . . . . . . 12 (𝑆 No → Ord dom 𝑆)
19971, 72, 1983syl 18 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord dom 𝑆)
200 ordtri2or 6483 . . . . . . . . . . 11 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord dom 𝑆) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
201197, 199, 200syl2anc 584 . . . . . . . . . 10 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
202139, 194, 201mpjaodan 960 . . . . . . . . 9 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 <s 𝑏)
203202ex 412 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍𝑏𝑍 <s 𝑏))
20456, 203biimtrrid 243 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏𝑍 <s 𝑏))
20555, 204mpd 15 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏)
206205expr 456 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆𝑍 <s 𝑏))
2078, 206sylbid 240 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏𝑍 <s 𝑏))
208207ralimdva 3164 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2091, 208biimtrid 242 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2102093impia 1116 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  ifcif 4530  {csn 4630  cop 4636   cuni 4911   cint 4950   class class class wbr 5147  cmpt 5230   Or wor 5595   × cxp 5686  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  Rel wrel 5693  Ord word 6384  Oncon0 6385  suc csuc 6387  cio 6513  Fun wfun 6556   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  crio 7386  1oc1o 8497  2oc2o 8498   No csur 27698   <s cslt 27699   bday cbday 27700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-1o 8504  df-2o 8505  df-no 27701  df-slt 27702  df-bday 27703
This theorem is referenced by:  noetalem1  27800
  Copyright terms: Public domain W3C validator