Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  noetalem3 Structured version   Visualization version   GIF version

Theorem noetalem3 33105
Description: Lemma for noeta 33108. 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
noetalem.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetalem.2 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
Assertion
Ref Expression
noetalem3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑔   𝑢,𝑎,𝐴,𝑣,𝑥,𝑦   𝐵,𝑎,𝑏   𝑔,𝑏,𝑥   𝑢,𝑔,𝑣,𝑥,𝑦   𝑆,𝑎,𝑔   𝑣,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑆(𝑥,𝑦,𝑣,𝑢,𝑏)   𝑍(𝑥,𝑦,𝑣,𝑢,𝑔,𝑎,𝑏)

Proof of Theorem noetalem3
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralcom 3358 . . 3 (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 ↔ ∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏)
2 simplll 771 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 No )
3 simpllr 772 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 ∈ V)
4 simprl 767 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐵 No )
54sselda 3970 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝑏 No )
6 noetalem.1 . . . . . . 7 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
76nosupbnd2 33102 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑏 No ) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
82, 3, 5, 7syl3anc 1365 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9 simpl 483 . . . . . . . . . . 11 ((𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏𝐵)
10 ssel2 3965 . . . . . . . . . . 11 ((𝐵 No 𝑏𝐵) → 𝑏 No )
114, 9, 10syl2an 595 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 No )
12 nodmord 33046 . . . . . . . . . 10 (𝑏 No → Ord dom 𝑏)
13 ordirr 6206 . . . . . . . . . 10 (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
1411, 12, 133syl 18 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15 ssun2 4152 . . . . . . . . . . 11 suc ( bday 𝐵) ⊆ (dom 𝑆 ∪ suc ( bday 𝐵))
16 bdayval 33041 . . . . . . . . . . . . . . 15 (𝑏 No → ( bday 𝑏) = dom 𝑏)
1711, 16syl 17 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) = dom 𝑏)
18 bdayfo 33068 . . . . . . . . . . . . . . . . 17 bday : No onto→On
19 fofn 6588 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → bday Fn No )
2018, 19ax-mp 5 . . . . . . . . . . . . . . . 16 bday Fn No
21 fnfvima 6992 . . . . . . . . . . . . . . . 16 (( bday Fn No 𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
2220, 21mp3an1 1441 . . . . . . . . . . . . . . 15 ((𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
234, 9, 22syl2an 595 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) ∈ ( bday 𝐵))
2417, 23eqeltrrd 2918 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday 𝐵))
25 elssuni 4865 . . . . . . . . . . . . 13 (dom 𝑏 ∈ ( bday 𝐵) → dom 𝑏 ( bday 𝐵))
2624, 25syl 17 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ( bday 𝐵))
27 nodmon 33043 . . . . . . . . . . . . 13 (𝑏 No → dom 𝑏 ∈ On)
28 imassrn 5937 . . . . . . . . . . . . . . . 16 ( bday 𝐵) ⊆ ran bday
29 forn 6589 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → ran bday = On)
3018, 29ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
3128, 30sseqtri 4006 . . . . . . . . . . . . . . 15 ( bday 𝐵) ⊆ On
32 ssorduni 7491 . . . . . . . . . . . . . . 15 (( bday 𝐵) ⊆ On → Ord ( bday 𝐵))
3331, 32ax-mp 5 . . . . . . . . . . . . . 14 Ord ( bday 𝐵)
34 ordsssuc 6274 . . . . . . . . . . . . . 14 ((dom 𝑏 ∈ On ∧ Ord ( bday 𝐵)) → (dom 𝑏 ( bday 𝐵) ↔ dom 𝑏 ∈ suc ( bday 𝐵)))
3533, 34mpan2 687 . . . . . . . . . . . . 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 233 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ( bday 𝐵))
3815, 37sseldi 3968 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)))
39 eleq2 2905 . . . . . . . . . 10 ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏))
4038, 39syl5ibcom 246 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏))
4114, 40mtod 199 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
42 noetalem.2 . . . . . . . . . . . 12 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
4342dmeqi 5771 . . . . . . . . . . 11 dom 𝑍 = dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
44 dmun 5777 . . . . . . . . . . 11 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
4543, 44eqtri 2848 . . . . . . . . . 10 dom 𝑍 = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
46 1oex 8104 . . . . . . . . . . . . 13 1o ∈ V
4746snnz 4709 . . . . . . . . . . . 12 {1o} ≠ ∅
48 dmxp 5797 . . . . . . . . . . . 12 ({1o} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆))
4947, 48ax-mp 5 . . . . . . . . . . 11 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆)
5049uneq2i 4139 . . . . . . . . . 10 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆))
51 undif2 4427 . . . . . . . . . 10 (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ( bday 𝐵))
5245, 50, 513eqtri 2852 . . . . . . . . 9 dom 𝑍 = (dom 𝑆 ∪ suc ( bday 𝐵))
53 dmeq 5770 . . . . . . . . 9 (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
5452, 53syl5eqr 2874 . . . . . . . 8 (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
5541, 54nsyl 142 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
56 df-ne 3021 . . . . . . . 8 (𝑍𝑏 ↔ ¬ 𝑍 = 𝑏)
57 notnotr 132 . . . . . . . . . . . . . . 15 (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆)
58 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
5958fvresd 6686 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
6042reseq1i 5847 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆)
61 resundir 5866 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆))
62 df-res 5565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V))
63 incom 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆))
64 disjdif 4423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅
6563, 64eqtri 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
66 xpdisj1 6015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅)
6765, 66ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ∩ (dom 𝑆 × V)) = ∅
6862, 67eqtri 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅
6968uneq2i 4139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
70 un0 4347 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
7169, 70eqtri 2848 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
7260, 61, 713eqtri 2852 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
73 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → (𝐴 No 𝐴 ∈ V))
746nosupno 33089 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑆 No )
7675adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑆 No )
77 nofun 33042 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑆 No → Fun 𝑆)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun 𝑆)
79 funrel 6368 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑆 → Rel 𝑆)
80 resdm 5895 . . . . . . . . . . . . . . . . . . . . . . . 24 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
8178, 79, 803syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
8272, 81syl5eq 2872 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
8382fveq1d 6668 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
8459, 83eqtr3d 2862 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
85 simp-4l 779 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 No )
86 simp-4r 780 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 ∈ V)
87 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
8887adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 ∈ V)
896, 42noetalem1 33103 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
9085, 86, 88, 89syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 No )
9190adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 No )
9211adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏 No )
9392adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑏 No )
94 simplr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍𝑏)
95 nosepne 33071 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 No 𝑏 No 𝑍𝑏) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9691, 93, 94, 95syl3anc 1365 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9784, 96eqnetrrd 3088 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9858fvresd 6686 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9997, 98neeqtrrd 3094 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
100 fveq2 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
101 fveq2 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (𝑆𝑞) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
102100, 101neeq12d 3081 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
103 df-ne 3021 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
104 necom 3073 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
105102, 103, 1043bitr3g 314 . . . . . . . . . . . . . . . . . . 19 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
106105rspcev 3626 . . . . . . . . . . . . . . . . . 18 (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∧ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
10758, 99, 106syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
108 rexeq 3411 . . . . . . . . . . . . . . . . 17 (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
109107, 108syl5ibrcom 248 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
110 rexnal 3242 . . . . . . . . . . . . . . . 16 (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
111109, 110syl6ib 252 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
11257, 111syl5 34 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
113112orrd 859 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
114 nofun 33042 . . . . . . . . . . . . . . . . 17 (𝑏 No → Fun 𝑏)
115 funres 6393 . . . . . . . . . . . . . . . . 17 (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
11693, 114, 1153syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
117 eqfunfv 6802 . . . . . . . . . . . . . . . 16 ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
118116, 78, 117syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
119 ianor 977 . . . . . . . . . . . . . . . 16 (¬ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
120119con1bii 358 . . . . . . . . . . . . . . 15 (¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
121118, 120syl6bbr 290 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ ¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
122121con2bid 356 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆))
123113, 122mpbid 233 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) = 𝑆)
124123pm2.21d 121 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆𝑍 <s 𝑏))
12582breq1d 5072 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
126 nodmon 33043 . . . . . . . . . . . . . 14 (𝑆 No → dom 𝑆 ∈ On)
12776, 126syl 17 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
128 sltres 33055 . . . . . . . . . . . . 13 ((𝑍 No 𝑏 No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
12991, 93, 127, 128syl3anc 1365 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
130125, 129sylbird 261 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
131 simplrr 774 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
132131adantr 481 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
133 noreson 33053 . . . . . . . . . . . . . . 15 ((𝑏 No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
13493, 127, 133syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
135 sltso 33067 . . . . . . . . . . . . . . 15 <s Or No
136 sotric 5499 . . . . . . . . . . . . . . 15 (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
137135, 136mpan 686 . . . . . . . . . . . . . 14 (((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
138134, 76, 137syl2anc 584 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
139138con2bid 356 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆)) ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
140132, 139mpbird 258 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆)))
141124, 130, 140mpjaod 856 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏)
14290adantr 481 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 No )
14392adantr 481 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏 No )
144 simplr 765 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍𝑏)
14542fveq1i 6667 . . . . . . . . . . . . 13 (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
146 simp-4l 779 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝐴 No 𝐴 ∈ V))
147146, 74, 773syl 18 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → Fun 𝑆)
148 funfn 6381 . . . . . . . . . . . . . . 15 (Fun 𝑆𝑆 Fn dom 𝑆)
149147, 148sylib 219 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑆 Fn dom 𝑆)
15046fconst 6561 . . . . . . . . . . . . . . . 16 ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}):(suc ( bday 𝐵) ∖ dom 𝑆)⟶{1o}
151 ffn 6510 . . . . . . . . . . . . . . . 16 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}):(suc ( bday 𝐵) ∖ dom 𝑆)⟶{1o} → ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ( bday 𝐵) ∖ dom 𝑆))
152150, 151ax-mp 5 . . . . . . . . . . . . . . 15 ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ( bday 𝐵) ∖ dom 𝑆)
153152a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) Fn (suc ( bday 𝐵) ∖ dom 𝑆))
15464a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅)
155 necom 3073 . . . . . . . . . . . . . . . . . . 19 ((𝑍𝑝) ≠ (𝑏𝑝) ↔ (𝑏𝑝) ≠ (𝑍𝑝))
156155rabbii 3478 . . . . . . . . . . . . . . . . . 18 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
157156inteqi 4877 . . . . . . . . . . . . . . . . 17 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
158144necomd 3075 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝑍)
159 nosepssdm 33076 . . . . . . . . . . . . . . . . . 18 ((𝑏 No 𝑍 No 𝑏𝑍) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
160143, 142, 158, 159syl3anc 1365 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
161157, 160eqsstrid 4018 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏)
162143, 16syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ( bday 𝑏) = dom 𝑏)
163 simplrl 773 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 No )
164163adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 No )
165164adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝐵 No )
166 simplrl 773 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏𝐵)
167166adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝐵)
168165, 167, 22syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ( bday 𝑏) ∈ ( bday 𝐵))
169162, 168eqeltrrd 2918 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ∈ ( bday 𝐵))
170169, 25syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ( bday 𝐵))
171143, 27, 353syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑏 ( bday 𝐵) ↔ dom 𝑏 ∈ suc ( bday 𝐵)))
172170, 171mpbid 233 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ∈ suc ( bday 𝐵))
173 nosepon 33058 . . . . . . . . . . . . . . . . . 18 ((𝑍 No 𝑏 No 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
174142, 143, 144, 173syl3anc 1365 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
175 eloni 6198 . . . . . . . . . . . . . . . . 17 ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
176 ordsuc 7520 . . . . . . . . . . . . . . . . . . 19 (Ord ( bday 𝐵) ↔ Ord suc ( bday 𝐵))
17733, 176mpbi 231 . . . . . . . . . . . . . . . . . 18 Ord suc ( bday 𝐵)
178 ordtr2 6232 . . . . . . . . . . . . . . . . . 18 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord suc ( bday 𝐵)) → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
179177, 178mpan2 687 . . . . . . . . . . . . . . . . 17 (Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
180174, 175, 1793syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
181161, 172, 180mp2and 695 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵))
182 simpr 485 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
183146, 74, 1263syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑆 ∈ On)
184 ontri1 6222 . . . . . . . . . . . . . . . . 17 ((dom 𝑆 ∈ On ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
185183, 174, 184syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
186182, 185mpbid 233 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
187181, 186eldifd 3950 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆))
188 fvun2 6751 . . . . . . . . . . . . . 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 ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
189149, 153, 154, 187, 188syl112anc 1368 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
190145, 189syl5eq 2872 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
19146fvconst2 6965 . . . . . . . . . . . . 13 ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆) → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o)
192187, 191syl 17 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o)
193190, 192eqtrd 2860 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o)
194 nosep1o 33072 . . . . . . . . . . 11 (((𝑍 No 𝑏 No 𝑍𝑏) ∧ (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1o) → 𝑍 <s 𝑏)
195142, 143, 144, 193, 194syl31anc 1367 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 <s 𝑏)
196 simpr 485 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍𝑏)
19790, 92, 196, 173syl3anc 1365 . . . . . . . . . . . 12 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
198197, 175syl 17 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
199 nodmord 33046 . . . . . . . . . . . 12 (𝑆 No → Ord dom 𝑆)
20073, 74, 1993syl 18 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord dom 𝑆)
201 ordtri2or 6283 . . . . . . . . . . 11 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord dom 𝑆) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
202198, 200, 201syl2anc 584 . . . . . . . . . 10 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
203141, 195, 202mpjaodan 954 . . . . . . . . 9 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 <s 𝑏)
204203ex 413 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍𝑏𝑍 <s 𝑏))
20556, 204syl5bir 244 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏𝑍 <s 𝑏))
20655, 205mpd 15 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏)
207206expr 457 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆𝑍 <s 𝑏))
2088, 207sylbid 241 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏𝑍 <s 𝑏))
209208ralimdva 3181 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2101, 209syl5bi 243 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2112103impia 1111 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2107  {cab 2803  wne 3020  wral 3142  wrex 3143  {crab 3146  Vcvv 3499  cdif 3936  cun 3937  cin 3938  wss 3939  c0 4294  ifcif 4469  {csn 4563  cop 4569   cuni 4836   cint 4873   class class class wbr 5062  cmpt 5142   Or wor 5471   × cxp 5551  dom cdm 5553  ran crn 5554  cres 5555  cima 5556  Rel wrel 5558  Ord word 6187  Oncon0 6188  suc csuc 6190  cio 6309  Fun wfun 6345   Fn wfn 6346  wf 6347  ontowfo 6349  cfv 6351  crio 7108  1oc1o 8089  2oc2o 8090   No csur 33033   <s cslt 33034   bday cbday 33035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-ord 6191  df-on 6192  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-1o 8096  df-2o 8097  df-no 33036  df-slt 33037  df-bday 33038
This theorem is referenced by:  noetalem5  33107
  Copyright terms: Public domain W3C validator