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

Theorem noinfbnd2lem1 27618
Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024.)
Assertion
Ref Expression
noinfbnd2lem1 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
Distinct variable groups:   𝐵,𝑏   𝑈,𝑏   𝑍,𝑏
Allowed substitution hints:   𝐵(𝑦)   𝑈(𝑦)   𝑉(𝑦,𝑏)   𝑍(𝑦)

Proof of Theorem noinfbnd2lem1
Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5145 . . 3 (𝑏 = 𝑈 → (𝑍 <s 𝑏𝑍 <s 𝑈))
2 simp3 1135 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
3 simp1l 1194 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑈𝐵)
41, 2, 3rspcdva 3607 . 2 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈)
5 simpl21 1248 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 No )
6 simpl1l 1221 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝐵)
75, 6sseldd 3978 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 No )
8 nodmon 27538 . . . . . . . . . 10 (𝑈 No → dom 𝑈 ∈ On)
97, 8syl 17 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10 onelon 6383 . . . . . . . . 9 ((dom 𝑈 ∈ On ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
119, 10sylan 579 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
12 simpr 484 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
13 simplr 766 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
149adantr 480 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
1514adantr 480 . . . . . . . . . . . . 13 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
16 ontr1 6404 . . . . . . . . . . . . 13 (dom 𝑈 ∈ On → ((𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
1715, 16syl 17 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
1812, 13, 17mp2and 696 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
1918fvresd 6905 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
20 onelon 6383 . . . . . . . . . . . . 13 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
2111, 20sylan 579 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
22 fveq2 6885 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
23 fveq2 6885 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
2422, 23neeq12d 2996 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
2524onnminsb 7784 . . . . . . . . . . . 12 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
2621, 12, 25sylc 65 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
27 df-ne 2935 . . . . . . . . . . . 12 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
2827con2bii 357 . . . . . . . . . . 11 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
2926, 28sylibr 233 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
3019, 29eqtr4d 2769 . . . . . . . . 9 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
3130ralrimiva 3140 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
32 simpr 484 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
3332fvresd 6905 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
34 simplr 766 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈)
35 simpl23 1250 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 No )
367adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
37 sltval2 27544 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No ) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3835, 36, 37syl2an2r 682 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3934, 38mpbid 231 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
40 necom 2988 . . . . . . . . . . . . 13 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
4140rabbii 3432 . . . . . . . . . . . 12 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4241inteqi 4947 . . . . . . . . . . 11 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4342fveq2i 6888 . . . . . . . . . 10 (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4442fveq2i 6888 . . . . . . . . . 10 (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4539, 43, 443brtr4g 5175 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
4633, 45eqbrtrd 5163 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
47 raleq 3316 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
48 fveq2 6885 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
49 fveq2 6885 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
5048, 49breq12d 5154 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝) ↔ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5147, 50anbi12d 630 . . . . . . . . 9 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
5251rspcev 3606 . . . . . . . 8 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
5311, 31, 46, 52syl12anc 834 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
54 noreson 27548 . . . . . . . . 9 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
5535, 9, 54syl2anc 583 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56 sltval 27535 . . . . . . . 8 (((𝑍 ↾ dom 𝑈) ∈ No 𝑈 No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝))))
5755, 36, 56syl2an2r 682 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝))))
5853, 57mpbird 257 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) <s 𝑈)
59 sssucid 6438 . . . . . . 7 dom 𝑈 ⊆ suc dom 𝑈
60 resabs1 6005 . . . . . . 7 (dom 𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
6159, 60mp1i 13 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
62 resundir 5990 . . . . . . 7 ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈))
63 nofun 27537 . . . . . . . . . . . . 13 (𝑈 No → Fun 𝑈)
647, 63syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65 funrel 6559 . . . . . . . . . . . 12 (Fun 𝑈 → Rel 𝑈)
6664, 65syl 17 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Rel 𝑈)
6766adantr 480 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Rel 𝑈)
68 resdm 6020 . . . . . . . . . 10 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
6967, 68syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70 nodmord 27541 . . . . . . . . . . . . 13 (𝑈 No → Ord dom 𝑈)
717, 70syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Ord dom 𝑈)
7271adantr 480 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Ord dom 𝑈)
73 ordirr 6376 . . . . . . . . . . 11 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
7472, 73syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75 1oex 8477 . . . . . . . . . . 11 1o ∈ V
7675snres0 6291 . . . . . . . . . 10 (({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
7774, 76sylibr 233 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅)
7869, 77uneq12d 4159 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79 un0 4385 . . . . . . . 8 (𝑈 ∪ ∅) = 𝑈
8078, 79eqtrdi 2782 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = 𝑈)
8162, 80eqtrid 2778 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = 𝑈)
8258, 61, 813brtr4d 5173 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈))
83 onsucb 7802 . . . . . . . . 9 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
849, 83sylib 217 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85 noreson 27548 . . . . . . . 8 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8635, 84, 85syl2anc 583 . . . . . . 7 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8786adantr 480 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8875prid1 4761 . . . . . . . . 9 1o ∈ {1o, 2o}
8988noextend 27554 . . . . . . . 8 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
907, 89syl 17 . . . . . . 7 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
9190adantr 480 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
92 sltres 27550 . . . . . 6 (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ∧ dom 𝑈 ∈ On) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩})))
9387, 91, 14, 92syl3anc 1368 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩})))
9482, 93mpd 15 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
95 sltso 27564 . . . . . 6 <s Or No
96 soasym 5612 . . . . . 6 (( <s Or No ∧ ((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9795, 96mpan 687 . . . . 5 (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9886, 91, 97syl2an2r 682 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9994, 98mpd 15 . . 3 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
100 sonr 5604 . . . . . 6 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
10195, 90, 100sylancr 586 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
102101adantr 480 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
103 df-suc 6364 . . . . . . . 8 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104103reseq2i 5972 . . . . . . 7 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105 resundi 5989 . . . . . . 7 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106104, 105eqtri 2754 . . . . . 6 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107 dmres 5997 . . . . . . . . 9 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
10842eqeq1i 2731 . . . . . . . . . . . . 13 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
109108biimpi 215 . . . . . . . . . . . 12 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
110109adantl 481 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
11135adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1127adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
113 simp23 1205 . . . . . . . . . . . . . . . . . 18 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 No )
114 sonr 5604 . . . . . . . . . . . . . . . . . 18 (( <s Or No 𝑍 No ) → ¬ 𝑍 <s 𝑍)
11595, 113, 114sylancr 586 . . . . . . . . . . . . . . . . 17 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
116 breq2 5145 . . . . . . . . . . . . . . . . . 18 (𝑈 = 𝑍 → (𝑍 <s 𝑈𝑍 <s 𝑍))
117116notbid 318 . . . . . . . . . . . . . . . . 17 (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
118115, 117syl5ibrcom 246 . . . . . . . . . . . . . . . 16 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
119118necon2ad 2949 . . . . . . . . . . . . . . 15 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈𝑈𝑍))
120119imp 406 . . . . . . . . . . . . . 14 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝑍)
121120necomd 2990 . . . . . . . . . . . . 13 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍𝑈)
122121adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
123 nosepssdm 27574 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
124111, 112, 122, 123syl3anc 1368 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
125110, 124eqsstrrd 4016 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
126 df-ss 3960 . . . . . . . . . 10 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127125, 126sylib 217 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
128107, 127eqtrid 2778 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
129128eleq2d 2813 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
130 simpr 484 . . . . . . . . . . . . 13 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
131130fvresd 6905 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
132112, 8syl 17 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ On)
133 onelon 6383 . . . . . . . . . . . . . . 15 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
134132, 133sylan 579 . . . . . . . . . . . . . 14 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
135 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
136135eleq2d 2813 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
137136biimpar 477 . . . . . . . . . . . . . 14 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
138134, 137, 25sylc 65 . . . . . . . . . . . . 13 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
139 nesym 2991 . . . . . . . . . . . . . 14 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
140139con2bii 357 . . . . . . . . . . . . 13 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
141138, 140sylibr 233 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
142131, 141eqtrd 2766 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
143142ex 412 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
144129, 143sylbid 239 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
145144ralrimiv 3139 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
146 nofun 27537 . . . . . . . . . . 11 (𝑍 No → Fun 𝑍)
147111, 146syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑍)
148147funresd 6585 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
14964adantr 480 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑈)
150 eqfunfv 7031 . . . . . . . . 9 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
151148, 149, 150syl2anc 583 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
152128, 145, 151mpbir2and 710 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
15335, 146syl 17 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍)
154153funfnd 6573 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 Fn dom 𝑍)
155112, 70syl 17 . . . . . . . . . . . . . . . 16 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
156155, 73syl 17 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
157 ndmfv 6920 . . . . . . . . . . . . . . . 16 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
158 2on0 8483 . . . . . . . . . . . . . . . . . . 19 2o ≠ ∅
159158necomi 2989 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2o
160 neeq1 2997 . . . . . . . . . . . . . . . . . 18 ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
161159, 160mpbiri 258 . . . . . . . . . . . . . . . . 17 ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2o)
162161neneqd 2939 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈) = ∅ → ¬ (𝑈‘dom 𝑈) = 2o)
163157, 162syl 17 . . . . . . . . . . . . . . 15 (¬ dom 𝑈 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑈) = 2o)
164156, 163syl 17 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 2o)
165164intnand 488 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o))
166 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈)
16735, 7, 37syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
168166, 167mpbid 231 . . . . . . . . . . . . . . . 16 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
169168adantr 480 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
170110fveq2d 6889 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑍‘dom 𝑈))
171110fveq2d 6889 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑈‘dom 𝑈))
172169, 170, 1713brtr3d 5172 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈))
173 fvex 6898 . . . . . . . . . . . . . . 15 (𝑍‘dom 𝑈) ∈ V
174 fvex 6898 . . . . . . . . . . . . . . 15 (𝑈‘dom 𝑈) ∈ V
175173, 174brtp 5516 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
176172, 175sylib 217 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
177 3orel3 1481 . . . . . . . . . . . . 13 (¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o) → ((((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o))))
178165, 176, 177sylc 65 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))
179 andi 1004 . . . . . . . . . . . 12 (((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))
180178, 179sylibr 233 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)))
181180simpld 494 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1o)
182 ndmfv 6920 . . . . . . . . . . . 12 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
183 1n0 8489 . . . . . . . . . . . . . . 15 1o ≠ ∅
184183necomi 2989 . . . . . . . . . . . . . 14 ∅ ≠ 1o
185 neeq1 2997 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
186184, 185mpbiri 258 . . . . . . . . . . . . 13 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1o)
187186neneqd 2939 . . . . . . . . . . . 12 ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 1o)
188182, 187syl 17 . . . . . . . . . . 11 (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 1o)
189188con4i 114 . . . . . . . . . 10 ((𝑍‘dom 𝑈) = 1o → dom 𝑈 ∈ dom 𝑍)
190181, 189syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
191 fnressn 7152 . . . . . . . . 9 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
192154, 190, 191syl2an2r 682 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
193181opeq2d 4875 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1o⟩)
194193sneqd 4635 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1o⟩})
195192, 194eqtrd 2766 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1o⟩})
196152, 195uneq12d 4159 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
197106, 196eqtrid 2778 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
198197breq2d 5153 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈) ↔ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩})))
199102, 198mtbird 325 . . 3 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
200 nosepssdm 27574 . . . . 5 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
2017, 35, 120, 200syl3anc 1368 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
202 nosepon 27553 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
2037, 35, 120, 202syl3anc 1368 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
204 onsseleq 6399 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
205203, 9, 204syl2anc 583 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
206201, 205mpbid 231 . . 3 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈))
20799, 199, 206mpjaodan 955 . 2 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
2084, 207mpdan 684 1 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  wne 2934  wral 3055  wrex 3064  {crab 3426  cun 3941  cin 3942  wss 3943  c0 4317  {csn 4623  {ctp 4627  cop 4629   cint 4943   class class class wbr 5141   Or wor 5580  dom cdm 5669  cres 5671  Rel wrel 5674  Ord word 6357  Oncon0 6358  suc csuc 6360  Fun wfun 6531   Fn wfn 6532  cfv 6537  1oc1o 8460  2oc2o 8461   No csur 27528   <s cslt 27529
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6361  df-on 6362  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-1o 8467  df-2o 8468  df-no 27531  df-slt 27532
This theorem is referenced by:  noinfbnd2  27619
  Copyright terms: Public domain W3C validator