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

Theorem noetalem3 31990
 Description: Lemma for noeta 31993. 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 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetalem.2 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
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 3127 . . 3 (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 ↔ ∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏)
2 simplll 813 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 No )
3 simpllr 815 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝐴 ∈ V)
4 simprl 809 . . . . . . 7 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐵 No )
54sselda 3636 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → 𝑏 No )
6 noetalem.1 . . . . . . 7 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
76nosupbnd2 31987 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑏 No ) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
82, 3, 5, 7syl3anc 1366 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏 ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
9 simpl 472 . . . . . . . . . . 11 ((𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆) → 𝑏𝐵)
10 ssel2 3631 . . . . . . . . . . 11 ((𝐵 No 𝑏𝐵) → 𝑏 No )
114, 9, 10syl2an 493 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑏 No )
12 nodmord 31931 . . . . . . . . . 10 (𝑏 No → Ord dom 𝑏)
13 ordirr 5779 . . . . . . . . . 10 (Ord dom 𝑏 → ¬ dom 𝑏 ∈ dom 𝑏)
1411, 12, 133syl 18 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ dom 𝑏 ∈ dom 𝑏)
15 ssun2 3810 . . . . . . . . . . 11 suc ( bday 𝐵) ⊆ (dom 𝑆 ∪ suc ( bday 𝐵))
16 bdayval 31926 . . . . . . . . . . . . . . 15 (𝑏 No → ( bday 𝑏) = dom 𝑏)
1711, 16syl 17 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) = dom 𝑏)
18 bdayfo 31953 . . . . . . . . . . . . . . . . 17 bday : No onto→On
19 fofn 6155 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → bday Fn No )
2018, 19ax-mp 5 . . . . . . . . . . . . . . . 16 bday Fn No
21 fnfvima 6536 . . . . . . . . . . . . . . . 16 (( bday Fn No 𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
2220, 21mp3an1 1451 . . . . . . . . . . . . . . 15 ((𝐵 No 𝑏𝐵) → ( bday 𝑏) ∈ ( bday 𝐵))
234, 9, 22syl2an 493 . . . . . . . . . . . . . 14 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ( bday 𝑏) ∈ ( bday 𝐵))
2417, 23eqeltrrd 2731 . . . . . . . . . . . . 13 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ ( bday 𝐵))
25 elssuni 4499 . . . . . . . . . . . . 13 (dom 𝑏 ∈ ( bday 𝐵) → dom 𝑏 ( bday 𝐵))
2624, 25syl 17 . . . . . . . . . . . 12 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ( bday 𝐵))
27 nodmon 31928 . . . . . . . . . . . . 13 (𝑏 No → dom 𝑏 ∈ On)
28 imassrn 5512 . . . . . . . . . . . . . . . 16 ( bday 𝐵) ⊆ ran bday
29 forn 6156 . . . . . . . . . . . . . . . . 17 ( bday : No onto→On → ran bday = On)
3018, 29ax-mp 5 . . . . . . . . . . . . . . . 16 ran bday = On
3128, 30sseqtri 3670 . . . . . . . . . . . . . . 15 ( bday 𝐵) ⊆ On
32 ssorduni 7027 . . . . . . . . . . . . . . 15 (( bday 𝐵) ⊆ On → Ord ( bday 𝐵))
3331, 32ax-mp 5 . . . . . . . . . . . . . 14 Ord ( bday 𝐵)
34 ordsssuc 5850 . . . . . . . . . . . . . 14 ((dom 𝑏 ∈ On ∧ Ord ( bday 𝐵)) → (dom 𝑏 ( bday 𝐵) ↔ dom 𝑏 ∈ suc ( bday 𝐵)))
3533, 34mpan2 707 . . . . . . . . . . . . 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 222 . . . . . . . . . . 11 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ suc ( bday 𝐵))
3815, 37sseldi 3634 . . . . . . . . . 10 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)))
39 eleq2 2719 . . . . . . . . . 10 ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → (dom 𝑏 ∈ (dom 𝑆 ∪ suc ( bday 𝐵)) ↔ dom 𝑏 ∈ dom 𝑏))
4038, 39syl5ibcom 235 . . . . . . . . 9 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ((dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏 → dom 𝑏 ∈ dom 𝑏))
4114, 40mtod 189 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
42 noetalem.2 . . . . . . . . . . . 12 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
4342dmeqi 5357 . . . . . . . . . . 11 dom 𝑍 = dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
44 dmun 5363 . . . . . . . . . . 11 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
4543, 44eqtri 2673 . . . . . . . . . 10 dom 𝑍 = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
46 1on 7612 . . . . . . . . . . . . . 14 1𝑜 ∈ On
4746elexi 3244 . . . . . . . . . . . . 13 1𝑜 ∈ V
4847snnz 4340 . . . . . . . . . . . 12 {1𝑜} ≠ ∅
49 dmxp 5376 . . . . . . . . . . . 12 ({1𝑜} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) = (suc ( bday 𝐵) ∖ dom 𝑆))
5048, 49ax-mp 5 . . . . . . . . . . 11 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) = (suc ( bday 𝐵) ∖ dom 𝑆)
5150uneq2i 3797 . . . . . . . . . 10 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆))
52 undif2 4077 . . . . . . . . . 10 (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ( bday 𝐵))
5345, 51, 523eqtri 2677 . . . . . . . . 9 dom 𝑍 = (dom 𝑆 ∪ suc ( bday 𝐵))
54 dmeq 5356 . . . . . . . . 9 (𝑍 = 𝑏 → dom 𝑍 = dom 𝑏)
5553, 54syl5eqr 2699 . . . . . . . 8 (𝑍 = 𝑏 → (dom 𝑆 ∪ suc ( bday 𝐵)) = dom 𝑏)
5641, 55nsyl 135 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → ¬ 𝑍 = 𝑏)
57 df-ne 2824 . . . . . . . 8 (𝑍𝑏 ↔ ¬ 𝑍 = 𝑏)
58 notnotr 125 . . . . . . . . . . . . . . 15 (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → dom (𝑏 ↾ dom 𝑆) = dom 𝑆)
59 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
6059fvresd 6246 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
6142reseq1i 5424 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) ↾ dom 𝑆)
62 resundir 5446 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ↾ dom 𝑆))
63 df-res 5155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ↾ dom 𝑆) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ∩ (dom 𝑆 × V))
64 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆))
65 disjdif 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅
6664, 65eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅
67 xpdisj1 5590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((suc ( bday 𝐵) ∖ dom 𝑆) ∩ dom 𝑆) = ∅ → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ∩ (dom 𝑆 × V)) = ∅)
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ∩ (dom 𝑆 × V)) = ∅
6963, 68eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ↾ dom 𝑆) = ∅
7069uneq2i 3797 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
71 un0 4000 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ↾ dom 𝑆)
7270, 71eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) ↾ dom 𝑆)) = (𝑆 ↾ dom 𝑆)
7361, 62, 723eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑍 ↾ dom 𝑆) = (𝑆 ↾ dom 𝑆)
74 simplll 813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → (𝐴 No 𝐴 ∈ V))
756nosupno 31974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑆 No )
7776adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑆 No )
78 nofun 31927 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑆 No → Fun 𝑆)
7977, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun 𝑆)
80 funrel 5943 . . . . . . . . . . . . . . . . . . . . . . . 24 (Fun 𝑆 → Rel 𝑆)
81 resdm 5476 . . . . . . . . . . . . . . . . . . . . . . . 24 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
8279, 80, 813syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 ↾ dom 𝑆) = 𝑆)
8373, 82syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 ↾ dom 𝑆) = 𝑆)
8483fveq1d 6231 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
8560, 84eqtr3d 2687 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
86 simp-4l 823 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 No )
87 simp-4r 824 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐴 ∈ V)
88 simplrr 818 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 ∈ V)
8988adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 ∈ V)
906, 42noetalem1 31988 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
9186, 87, 89, 90syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 No )
9291adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 No )
9311adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏 No )
9493adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑏 No )
95 simplr 807 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍𝑏)
96 nosepne 31956 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 No 𝑏 No 𝑍𝑏) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9792, 94, 95, 96syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9885, 97eqnetrrd 2891 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
9959fvresd 6246 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (𝑏 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
10098, 99neeqtrrd 2897 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
101 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → ((𝑏 ↾ dom 𝑆)‘𝑞) = ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
102 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (𝑆𝑞) = (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
103101, 102neeq12d 2884 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
104 df-ne 2824 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘𝑞) ≠ (𝑆𝑞) ↔ ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
105 necom 2876 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
106103, 104, 1053bitr3g 302 . . . . . . . . . . . . . . . . . . 19 (𝑞 = {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})))
107106rspcev 3340 . . . . . . . . . . . . . . . . . 18 (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∧ (𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) ≠ ((𝑏 ↾ dom 𝑆)‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
10859, 100, 107syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
109 rexeq 3169 . . . . . . . . . . . . . . . . 17 (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ ∃𝑞 ∈ dom 𝑆 ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
110108, 109syl5ibrcom 237 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
111 rexnal 3024 . . . . . . . . . . . . . . . 16 (∃𝑞 ∈ dom (𝑏 ↾ dom 𝑆) ¬ ((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞) ↔ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))
112110, 111syl6ib 241 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
11358, 112syl5 34 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (¬ ¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 → ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
114113orrd 392 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
115 nofun 31927 . . . . . . . . . . . . . . . . 17 (𝑏 No → Fun 𝑏)
116 funres 5967 . . . . . . . . . . . . . . . . 17 (Fun 𝑏 → Fun (𝑏 ↾ dom 𝑆))
11794, 115, 1163syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → Fun (𝑏 ↾ dom 𝑆))
118 eqfunfv 6356 . . . . . . . . . . . . . . . 16 ((Fun (𝑏 ↾ dom 𝑆) ∧ Fun 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
119117, 79, 118syl2anc 694 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
120 ianor 508 . . . . . . . . . . . . . . . 16 (¬ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
121120con1bii 345 . . . . . . . . . . . . . . 15 (¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ (dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∧ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)))
122119, 121syl6bbr 278 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆 ↔ ¬ (¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞))))
123122con2bid 343 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((¬ dom (𝑏 ↾ dom 𝑆) = dom 𝑆 ∨ ¬ ∀𝑞 ∈ dom (𝑏 ↾ dom 𝑆)((𝑏 ↾ dom 𝑆)‘𝑞) = (𝑆𝑞)) ↔ ¬ (𝑏 ↾ dom 𝑆) = 𝑆))
124114, 123mpbid 222 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) = 𝑆)
125124pm2.21d 118 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆𝑍 <s 𝑏))
12683breq1d 4695 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) ↔ 𝑆 <s (𝑏 ↾ dom 𝑆)))
127 nodmon 31928 . . . . . . . . . . . . . 14 (𝑆 No → dom 𝑆 ∈ On)
12877, 127syl 17 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → dom 𝑆 ∈ On)
129 sltres 31940 . . . . . . . . . . . . 13 ((𝑍 No 𝑏 No ∧ dom 𝑆 ∈ On) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
13092, 94, 128, 129syl3anc 1366 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
131126, 130sylbird 250 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑆 <s (𝑏 ↾ dom 𝑆) → 𝑍 <s 𝑏))
132 simplrr 818 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
133132adantr 480 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)
134 noreson 31938 . . . . . . . . . . . . . . 15 ((𝑏 No ∧ dom 𝑆 ∈ On) → (𝑏 ↾ dom 𝑆) ∈ No )
13594, 128, 134syl2anc 694 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (𝑏 ↾ dom 𝑆) ∈ No )
136 sltso 31952 . . . . . . . . . . . . . . 15 <s Or No
137 sotric 5090 . . . . . . . . . . . . . . 15 (( <s Or No ∧ ((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No )) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
138136, 137mpan 706 . . . . . . . . . . . . . 14 (((𝑏 ↾ dom 𝑆) ∈ No 𝑆 No ) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
139135, 77, 138syl2anc 694 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) <s 𝑆 ↔ ¬ ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆))))
140139con2bid 343 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → (((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆)) ↔ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆))
141133, 140mpbird 247 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → ((𝑏 ↾ dom 𝑆) = 𝑆𝑆 <s (𝑏 ↾ dom 𝑆)))
142125, 131, 141mpjaod 395 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆) → 𝑍 <s 𝑏)
14391adantr 480 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 No )
14493adantr 480 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏 No )
145 simplr 807 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍𝑏)
14642fveq1i 6230 . . . . . . . . . . . . 13 (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
147 simp-4l 823 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝐴 No 𝐴 ∈ V))
148147, 75, 783syl 18 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → Fun 𝑆)
149 funfn 5956 . . . . . . . . . . . . . . 15 (Fun 𝑆𝑆 Fn dom 𝑆)
150148, 149sylib 208 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑆 Fn dom 𝑆)
15147fconst 6129 . . . . . . . . . . . . . . . 16 ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}):(suc ( bday 𝐵) ∖ dom 𝑆)⟶{1𝑜}
152 ffn 6083 . . . . . . . . . . . . . . . 16 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}):(suc ( bday 𝐵) ∖ dom 𝑆)⟶{1𝑜} → ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) Fn (suc ( bday 𝐵) ∖ dom 𝑆))
153151, 152ax-mp 5 . . . . . . . . . . . . . . 15 ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) Fn (suc ( bday 𝐵) ∖ dom 𝑆)
154153a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) Fn (suc ( bday 𝐵) ∖ dom 𝑆))
15565a1i 11 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅)
156 necom 2876 . . . . . . . . . . . . . . . . . . 19 ((𝑍𝑝) ≠ (𝑏𝑝) ↔ (𝑏𝑝) ≠ (𝑍𝑝))
157156rabbii 3216 . . . . . . . . . . . . . . . . . 18 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
158157inteqi 4511 . . . . . . . . . . . . . . . . 17 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} = {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)}
159145necomd 2878 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝑍)
160 nosepssdm 31961 . . . . . . . . . . . . . . . . . 18 ((𝑏 No 𝑍 No 𝑏𝑍) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
161144, 143, 159, 160syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑏𝑝) ≠ (𝑍𝑝)} ⊆ dom 𝑏)
162158, 161syl5eqss 3682 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏)
163144, 16syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ( bday 𝑏) = dom 𝑏)
164 simplrl 817 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝐵 No )
165164adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝐵 No )
166165adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝐵 No )
167 simplrl 817 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑏𝐵)
168167adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑏𝐵)
169166, 168, 22syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ( bday 𝑏) ∈ ( bday 𝐵))
170163, 169eqeltrrd 2731 . . . . . . . . . . . . . . . . . 18 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ∈ ( bday 𝐵))
171170, 25syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ( bday 𝐵))
172144, 27, 353syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑏 ( bday 𝐵) ↔ dom 𝑏 ∈ suc ( bday 𝐵)))
173171, 172mpbid 222 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑏 ∈ suc ( bday 𝐵))
174 nosepon 31943 . . . . . . . . . . . . . . . . . 18 ((𝑍 No 𝑏 No 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
175143, 144, 145, 174syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
176 eloni 5771 . . . . . . . . . . . . . . . . 17 ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
177 ordsuc 7056 . . . . . . . . . . . . . . . . . . 19 (Ord ( bday 𝐵) ↔ Ord suc ( bday 𝐵))
17833, 177mpbi 220 . . . . . . . . . . . . . . . . . 18 Ord suc ( bday 𝐵)
179 ordtr2 5806 . . . . . . . . . . . . . . . . . 18 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord suc ( bday 𝐵)) → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
180178, 179mpan2 707 . . . . . . . . . . . . . . . . 17 (Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
181175, 176, 1803syl 18 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ⊆ dom 𝑏 ∧ dom 𝑏 ∈ suc ( bday 𝐵)) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵)))
182162, 173, 181mp2and 715 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ suc ( bday 𝐵))
183 simpr 476 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
184147, 75, 1273syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → dom 𝑆 ∈ On)
185 ontri1 5795 . . . . . . . . . . . . . . . . 17 ((dom 𝑆 ∈ On ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
186184, 175, 185syl2anc 694 . . . . . . . . . . . . . . . 16 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ↔ ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆))
187183, 186mpbid 222 . . . . . . . . . . . . . . 15 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ¬ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆)
188182, 187eldifd 3618 . . . . . . . . . . . . . 14 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆))
189 fvun2 6309 . . . . . . . . . . . . . 14 ((𝑆 Fn dom 𝑆 ∧ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) Fn (suc ( bday 𝐵) ∖ dom 𝑆) ∧ ((dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅ ∧ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆))) → ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
190150, 154, 155, 188, 189syl112anc 1370 . . . . . . . . . . . . 13 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
191146, 190syl5eq 2697 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
19247fvconst2 6510 . . . . . . . . . . . . 13 ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ (suc ( bday 𝐵) ∖ dom 𝑆) → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1𝑜)
193188, 192syl 17 . . . . . . . . . . . 12 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})‘ {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1𝑜)
194191, 193eqtrd 2685 . . . . . . . . . . 11 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1𝑜)
195 nosep1o 31957 . . . . . . . . . . 11 (((𝑍 No 𝑏 No 𝑍𝑏) ∧ (𝑍 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) = 1𝑜) → 𝑍 <s 𝑏)
196143, 144, 145, 194, 195syl31anc 1369 . . . . . . . . . 10 ((((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) ∧ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}) → 𝑍 <s 𝑏)
197 simpr 476 . . . . . . . . . . . . 13 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍𝑏)
19891, 93, 197, 174syl3anc 1366 . . . . . . . . . . . 12 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ On)
199198, 176syl 17 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)})
200 nodmord 31931 . . . . . . . . . . . 12 (𝑆 No → Ord dom 𝑆)
20174, 75, 2003syl 18 . . . . . . . . . . 11 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → Ord dom 𝑆)
202 ordtri2or 5860 . . . . . . . . . . 11 ((Ord {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∧ Ord dom 𝑆) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
203199, 201, 202syl2anc 694 . . . . . . . . . 10 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → ( {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)} ∈ dom 𝑆 ∨ dom 𝑆 {𝑝 ∈ On ∣ (𝑍𝑝) ≠ (𝑏𝑝)}))
204142, 196, 203mpjaodan 844 . . . . . . . . 9 (((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) ∧ 𝑍𝑏) → 𝑍 <s 𝑏)
205204ex 449 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (𝑍𝑏𝑍 <s 𝑏))
20657, 205syl5bir 233 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → (¬ 𝑍 = 𝑏𝑍 <s 𝑏))
20756, 206mpd 15 . . . . . 6 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ (𝑏𝐵 ∧ ¬ (𝑏 ↾ dom 𝑆) <s 𝑆)) → 𝑍 <s 𝑏)
208207expr 642 . . . . 5 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (¬ (𝑏 ↾ dom 𝑆) <s 𝑆𝑍 <s 𝑏))
2098, 208sylbid 230 . . . 4 ((((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) ∧ 𝑏𝐵) → (∀𝑎𝐴 𝑎 <s 𝑏𝑍 <s 𝑏))
210209ralimdva 2991 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑏𝐵𝑎𝐴 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2111, 210syl5bi 232 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏 → ∀𝑏𝐵 𝑍 <s 𝑏))
2122113impia 1280 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V) ∧ ∀𝑎𝐴𝑏𝐵 𝑎 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  {cab 2637   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {csn 4210  ⟨cop 4216  ∪ cuni 4468  ∩ cint 4507   class class class wbr 4685   ↦ cmpt 4762   Or wor 5063   × cxp 5141  dom cdm 5143  ran crn 5144   ↾ cres 5145   “ cima 5146  Rel wrel 5148  Ord word 5760  Oncon0 5761  suc csuc 5763  ℩cio 5887  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  ℩crio 6650  1𝑜c1o 7598  2𝑜c2o 7599   No csur 31918
 Copyright terms: Public domain W3C validator