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

Theorem noinfbnd2lem1 33530
 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 5040 . . 3 (𝑏 = 𝑈 → (𝑍 <s 𝑏𝑍 <s 𝑈))
2 simp3 1135 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
3 simp1l 1194 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑈𝐵)
41, 2, 3rspcdva 3545 . 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 3895 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 No )
8 nodmon 33450 . . . . . . . . . 10 (𝑈 No → dom 𝑈 ∈ On)
97, 8syl 17 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10 onelon 6199 . . . . . . . . 9 ((dom 𝑈 ∈ On ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
119, 10sylan 583 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
12 simpr 488 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
13 simplr 768 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
149adantr 484 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
1514adantr 484 . . . . . . . . . . . . 13 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
16 ontr1 6220 . . . . . . . . . . . . 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 698 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
1918fvresd 6683 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
20 onelon 6199 . . . . . . . . . . . . 13 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
2111, 20sylan 583 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
22 fveq2 6663 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
23 fveq2 6663 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
2422, 23neeq12d 3012 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
2524onnminsb 7524 . . . . . . . . . . . 12 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
2621, 12, 25sylc 65 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
27 df-ne 2952 . . . . . . . . . . . 12 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
2827con2bii 361 . . . . . . . . . . 11 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
2926, 28sylibr 237 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
3019, 29eqtr4d 2796 . . . . . . . . 9 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
3130ralrimiva 3113 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
32 simpr 488 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
3332fvresd 6683 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
34 simplr 768 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈)
35 simpl23 1250 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 No )
367adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
37 sltval2 33456 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No ) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3835, 36, 37syl2an2r 684 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3934, 38mpbid 235 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
40 necom 3004 . . . . . . . . . . . . 13 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
4140rabbii 3385 . . . . . . . . . . . 12 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4241inteqi 4845 . . . . . . . . . . 11 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4342fveq2i 6666 . . . . . . . . . 10 (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4442fveq2i 6666 . . . . . . . . . 10 (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4539, 43, 443brtr4g 5070 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
4633, 45eqbrtrd 5058 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
47 raleq 3323 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
48 fveq2 6663 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
49 fveq2 6663 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
5048, 49breq12d 5049 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝) ↔ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5147, 50anbi12d 633 . . . . . . . . 9 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
5251rspcev 3543 . . . . . . . 8 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
5311, 31, 46, 52syl12anc 835 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
54 noreson 33460 . . . . . . . . 9 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
5535, 9, 54syl2anc 587 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56 sltval 33447 . . . . . . . 8 (((𝑍 ↾ dom 𝑈) ∈ No 𝑈 No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝))))
5755, 36, 56syl2an2r 684 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝))))
5853, 57mpbird 260 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) <s 𝑈)
59 sssucid 6251 . . . . . . 7 dom 𝑈 ⊆ suc dom 𝑈
60 resabs1 5858 . . . . . . 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 5843 . . . . . . 7 ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈))
63 nofun 33449 . . . . . . . . . . . . 13 (𝑈 No → Fun 𝑈)
647, 63syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65 funrel 6357 . . . . . . . . . . . 12 (Fun 𝑈 → Rel 𝑈)
6664, 65syl 17 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Rel 𝑈)
6766adantr 484 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Rel 𝑈)
68 resdm 5873 . . . . . . . . . 10 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
6967, 68syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70 nodmord 33453 . . . . . . . . . . . . 13 (𝑈 No → Ord dom 𝑈)
717, 70syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Ord dom 𝑈)
7271adantr 484 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Ord dom 𝑈)
73 ordirr 6192 . . . . . . . . . . 11 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
7472, 73syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75 1oex 8126 . . . . . . . . . . 11 1o ∈ V
7675snres0 33205 . . . . . . . . . 10 (({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
7774, 76sylibr 237 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅)
7869, 77uneq12d 4071 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79 un0 4289 . . . . . . . 8 (𝑈 ∪ ∅) = 𝑈
8078, 79eqtrdi 2809 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = 𝑈)
8162, 80syl5eq 2805 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = 𝑈)
8258, 61, 813brtr4d 5068 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈))
83 sucelon 7537 . . . . . . . . 9 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
849, 83sylib 221 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85 noreson 33460 . . . . . . . 8 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8635, 84, 85syl2anc 587 . . . . . . 7 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8786adantr 484 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8875prid1 4658 . . . . . . . . 9 1o ∈ {1o, 2o}
8988noextend 33466 . . . . . . . 8 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
907, 89syl 17 . . . . . . 7 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
9190adantr 484 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )
92 sltres 33462 . . . . . 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 33476 . . . . . 6 <s Or No
96 soasym 5477 . . . . . 6 (( <s Or No ∧ ((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9795, 96mpan 689 . . . . 5 (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9886, 91, 97syl2an2r 684 . . . 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 5469 . . . . . 6 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
10195, 90, 100sylancr 590 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
102101adantr 484 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
103 df-suc 6180 . . . . . . . 8 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104103reseq2i 5825 . . . . . . 7 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105 resundi 5842 . . . . . . 7 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106104, 105eqtri 2781 . . . . . 6 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107 dmres 5850 . . . . . . . . 9 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
10842eqeq1i 2763 . . . . . . . . . . . . 13 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
109108biimpi 219 . . . . . . . . . . . 12 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
110109adantl 485 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
11135adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1127adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
113 simp23 1205 . . . . . . . . . . . . . . . . . 18 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 No )
114 sonr 5469 . . . . . . . . . . . . . . . . . 18 (( <s Or No 𝑍 No ) → ¬ 𝑍 <s 𝑍)
11595, 113, 114sylancr 590 . . . . . . . . . . . . . . . . 17 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
116 breq2 5040 . . . . . . . . . . . . . . . . . 18 (𝑈 = 𝑍 → (𝑍 <s 𝑈𝑍 <s 𝑍))
117116notbid 321 . . . . . . . . . . . . . . . . 17 (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
118115, 117syl5ibrcom 250 . . . . . . . . . . . . . . . 16 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
119118necon2ad 2966 . . . . . . . . . . . . . . 15 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈𝑈𝑍))
120119imp 410 . . . . . . . . . . . . . 14 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝑍)
121120necomd 3006 . . . . . . . . . . . . 13 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍𝑈)
122121adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
123 nosepssdm 33486 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
124111, 112, 122, 123syl3anc 1368 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
125110, 124eqsstrrd 3933 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
126 df-ss 3877 . . . . . . . . . 10 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127125, 126sylib 221 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
128107, 127syl5eq 2805 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
129128eleq2d 2837 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
130 simpr 488 . . . . . . . . . . . . 13 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
131130fvresd 6683 . . . . . . . . . . . 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 6199 . . . . . . . . . . . . . . 15 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
134132, 133sylan 583 . . . . . . . . . . . . . 14 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
135 simpr 488 . . . . . . . . . . . . . . . 16 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
136135eleq2d 2837 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
137136biimpar 481 . . . . . . . . . . . . . 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 3007 . . . . . . . . . . . . . 14 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
140139con2bii 361 . . . . . . . . . . . . 13 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
141138, 140sylibr 237 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
142131, 141eqtrd 2793 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
143142ex 416 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
144129, 143sylbid 243 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
145144ralrimiv 3112 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
146 nofun 33449 . . . . . . . . . . 11 (𝑍 No → Fun 𝑍)
147111, 146syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑍)
148147funresd 6383 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
14964adantr 484 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑈)
150 eqfunfv 6803 . . . . . . . . 9 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
151148, 149, 150syl2anc 587 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
152128, 145, 151mpbir2and 712 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
15335, 146syl 17 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍)
154153funfnd 6371 . . . . . . . . 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 6693 . . . . . . . . . . . . . . . 16 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
158 2on0 8129 . . . . . . . . . . . . . . . . . . 19 2o ≠ ∅
159158necomi 3005 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2o
160 neeq1 3013 . . . . . . . . . . . . . . . . . 18 ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
161159, 160mpbiri 261 . . . . . . . . . . . . . . . . 17 ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2o)
162161neneqd 2956 . . . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o))
166 simpr 488 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈)
16735, 7, 37syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
168166, 167mpbid 235 . . . . . . . . . . . . . . . 16 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
169168adantr 484 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
170110fveq2d 6667 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑍‘dom 𝑈))
171110fveq2d 6667 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑈‘dom 𝑈))
172169, 170, 1713brtr3d 5067 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈))
173 fvex 6676 . . . . . . . . . . . . . . 15 (𝑍‘dom 𝑈) ∈ V
174 fvex 6676 . . . . . . . . . . . . . . 15 (𝑈‘dom 𝑈) ∈ V
175173, 174brtp 33244 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
176172, 175sylib 221 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
177 3orel3 33185 . . . . . . . . . . . . 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 1005 . . . . . . . . . . . 12 (((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))
180178, 179sylibr 237 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)))
181180simpld 498 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1o)
182 ndmfv 6693 . . . . . . . . . . . 12 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
183 1n0 8135 . . . . . . . . . . . . . . 15 1o ≠ ∅
184183necomi 3005 . . . . . . . . . . . . . 14 ∅ ≠ 1o
185 neeq1 3013 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
186184, 185mpbiri 261 . . . . . . . . . . . . 13 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1o)
187186neneqd 2956 . . . . . . . . . . . 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 6917 . . . . . . . . 9 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
192154, 190, 191syl2an2r 684 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
193181opeq2d 4773 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1o⟩)
194193sneqd 4537 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1o⟩})
195192, 194eqtrd 2793 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1o⟩})
196152, 195uneq12d 4071 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
197106, 196syl5eq 2805 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
198197breq2d 5048 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈) ↔ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩})))
199102, 198mtbird 328 . . 3 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
200 nosepssdm 33486 . . . . 5 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
2017, 35, 120, 200syl3anc 1368 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
202 nosepon 33465 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
2037, 35, 120, 202syl3anc 1368 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
204 onsseleq 6215 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
205203, 9, 204syl2anc 587 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
206201, 205mpbid 235 . . 3 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈))
20799, 199, 206mpjaodan 956 . 2 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
2084, 207mpdan 686 1 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  {crab 3074   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  {csn 4525  {ctp 4529  ⟨cop 4531  ∩ cint 4841   class class class wbr 5036   Or wor 5446  dom cdm 5528   ↾ cres 5530  Rel wrel 5533  Ord word 6173  Oncon0 6174  suc csuc 6176  Fun wfun 6334   Fn wfn 6335  ‘cfv 6340  1oc1o 8111  2oc2o 8112   No csur 33440
 Copyright terms: Public domain W3C validator