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

Theorem noinfbnd2lem1 27576
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 5152 . . 3 (𝑏 = 𝑈 → (𝑍 <s 𝑏𝑍 <s 𝑈))
2 simp3 1137 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
3 simp1l 1196 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑈𝐵)
41, 2, 3rspcdva 3613 . 2 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈)
5 simpl21 1250 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 No )
6 simpl1l 1223 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝐵)
75, 6sseldd 3983 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 No )
8 nodmon 27496 . . . . . . . . . 10 (𝑈 No → dom 𝑈 ∈ On)
97, 8syl 17 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10 onelon 6389 . . . . . . . . 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 6410 . . . . . . . . . . . . 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 6911 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
20 onelon 6389 . . . . . . . . . . . . 13 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
2111, 20sylan 579 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
22 fveq2 6891 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
23 fveq2 6891 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
2422, 23neeq12d 3001 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
2524onnminsb 7791 . . . . . . . . . . . 12 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
2621, 12, 25sylc 65 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
27 df-ne 2940 . . . . . . . . . . . 12 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
2827con2bii 357 . . . . . . . . . . 11 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
2926, 28sylibr 233 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
3019, 29eqtr4d 2774 . . . . . . . . 9 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
3130ralrimiva 3145 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
32 simpr 484 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
3332fvresd 6911 . . . . . . . . 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 1252 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 No )
367adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
37 sltval2 27502 . . . . . . . . . . . 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 2993 . . . . . . . . . . . . 13 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
4140rabbii 3437 . . . . . . . . . . . 12 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4241inteqi 4954 . . . . . . . . . . 11 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4342fveq2i 6894 . . . . . . . . . 10 (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4442fveq2i 6894 . . . . . . . . . 10 (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4539, 43, 443brtr4g 5182 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
4633, 45eqbrtrd 5170 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
47 raleq 3321 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
48 fveq2 6891 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
49 fveq2 6891 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
5048, 49breq12d 5161 . . . . . . . . . 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 3612 . . . . . . . 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 27506 . . . . . . . . 9 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
5535, 9, 54syl2anc 583 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56 sltval 27493 . . . . . . . 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 6444 . . . . . . 7 dom 𝑈 ⊆ suc dom 𝑈
60 resabs1 6011 . . . . . . 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 5996 . . . . . . 7 ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈))
63 nofun 27495 . . . . . . . . . . . . 13 (𝑈 No → Fun 𝑈)
647, 63syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65 funrel 6565 . . . . . . . . . . . 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 6026 . . . . . . . . . 10 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
6967, 68syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70 nodmord 27499 . . . . . . . . . . . . 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 6382 . . . . . . . . . . 11 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
7472, 73syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75 1oex 8482 . . . . . . . . . . 11 1o ∈ V
7675snres0 6297 . . . . . . . . . 10 (({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
7774, 76sylibr 233 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅)
7869, 77uneq12d 4164 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79 un0 4390 . . . . . . . 8 (𝑈 ∪ ∅) = 𝑈
8078, 79eqtrdi 2787 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = 𝑈)
8162, 80eqtrid 2783 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = 𝑈)
8258, 61, 813brtr4d 5180 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈))
83 onsucb 7809 . . . . . . . . 9 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
849, 83sylib 217 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85 noreson 27506 . . . . . . . 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 4766 . . . . . . . . 9 1o ∈ {1o, 2o}
8988noextend 27512 . . . . . . . 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 27508 . . . . . 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 1370 . . . . 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 27522 . . . . . 6 <s Or No
96 soasym 5619 . . . . . 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 5611 . . . . . 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 6370 . . . . . . . 8 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104103reseq2i 5978 . . . . . . 7 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105 resundi 5995 . . . . . . 7 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106104, 105eqtri 2759 . . . . . 6 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107 dmres 6003 . . . . . . . . 9 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
10842eqeq1i 2736 . . . . . . . . . . . . 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 1207 . . . . . . . . . . . . . . . . . 18 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 No )
114 sonr 5611 . . . . . . . . . . . . . . . . . 18 (( <s Or No 𝑍 No ) → ¬ 𝑍 <s 𝑍)
11595, 113, 114sylancr 586 . . . . . . . . . . . . . . . . 17 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
116 breq2 5152 . . . . . . . . . . . . . . . . . 18 (𝑈 = 𝑍 → (𝑍 <s 𝑈𝑍 <s 𝑍))
117116notbid 318 . . . . . . . . . . . . . . . . 17 (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
118115, 117syl5ibrcom 246 . . . . . . . . . . . . . . . 16 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
119118necon2ad 2954 . . . . . . . . . . . . . . 15 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈𝑈𝑍))
120119imp 406 . . . . . . . . . . . . . 14 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝑍)
121120necomd 2995 . . . . . . . . . . . . 13 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍𝑈)
122121adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
123 nosepssdm 27532 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
124111, 112, 122, 123syl3anc 1370 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
125110, 124eqsstrrd 4021 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
126 df-ss 3965 . . . . . . . . . 10 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127125, 126sylib 217 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
128107, 127eqtrid 2783 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
129128eleq2d 2818 . . . . . . . . . 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 6911 . . . . . . . . . . . 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 6389 . . . . . . . . . . . . . . 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 2818 . . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . 14 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
140139con2bii 357 . . . . . . . . . . . . 13 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
141138, 140sylibr 233 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
142131, 141eqtrd 2771 . . . . . . . . . . 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 3144 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
146 nofun 27495 . . . . . . . . . . 11 (𝑍 No → Fun 𝑍)
147111, 146syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑍)
148147funresd 6591 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
14964adantr 480 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑈)
150 eqfunfv 7037 . . . . . . . . 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 6579 . . . . . . . . 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 6926 . . . . . . . . . . . . . . . 16 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
158 2on0 8488 . . . . . . . . . . . . . . . . . . 19 2o ≠ ∅
159158necomi 2994 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2o
160 neeq1 3002 . . . . . . . . . . . . . . . . . 18 ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
161159, 160mpbiri 258 . . . . . . . . . . . . . . . . 17 ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2o)
162161neneqd 2944 . . . . . . . . . . . . . . . 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 6895 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑍‘dom 𝑈))
171110fveq2d 6895 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑈‘dom 𝑈))
172169, 170, 1713brtr3d 5179 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈))
173 fvex 6904 . . . . . . . . . . . . . . 15 (𝑍‘dom 𝑈) ∈ V
174 fvex 6904 . . . . . . . . . . . . . . 15 (𝑈‘dom 𝑈) ∈ V
175173, 174brtp 5523 . . . . . . . . . . . . . 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 1485 . . . . . . . . . . . . 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 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 6926 . . . . . . . . . . . 12 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
183 1n0 8494 . . . . . . . . . . . . . . 15 1o ≠ ∅
184183necomi 2994 . . . . . . . . . . . . . 14 ∅ ≠ 1o
185 neeq1 3002 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
186184, 185mpbiri 258 . . . . . . . . . . . . 13 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1o)
187186neneqd 2944 . . . . . . . . . . . 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 7158 . . . . . . . . 9 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
192154, 190, 191syl2an2r 682 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
193181opeq2d 4880 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1o⟩)
194193sneqd 4640 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1o⟩})
195192, 194eqtrd 2771 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1o⟩})
196152, 195uneq12d 4164 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
197106, 196eqtrid 2783 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
198197breq2d 5160 . . . 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 27532 . . . . 5 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
2017, 35, 120, 200syl3anc 1370 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
202 nosepon 27511 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
2037, 35, 120, 202syl3anc 1370 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
204 onsseleq 6405 . . . . 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 956 . 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 1085  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  {crab 3431  cun 3946  cin 3947  wss 3948  c0 4322  {csn 4628  {ctp 4632  cop 4634   cint 4950   class class class wbr 5148   Or wor 5587  dom cdm 5676  cres 5678  Rel wrel 5681  Ord word 6363  Oncon0 6364  suc csuc 6366  Fun wfun 6537   Fn wfn 6538  cfv 6543  1oc1o 8465  2oc2o 8466   No csur 27486   <s cslt 27487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-1o 8472  df-2o 8473  df-no 27489  df-slt 27490
This theorem is referenced by:  noinfbnd2  27577
  Copyright terms: Public domain W3C validator