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

Theorem noinfbnd2lem1 27775
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 5147 . . 3 (𝑏 = 𝑈 → (𝑍 <s 𝑏𝑍 <s 𝑈))
2 simp3 1139 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ∀𝑏𝐵 𝑍 <s 𝑏)
3 simp1l 1198 . . 3 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑈𝐵)
41, 2, 3rspcdva 3623 . 2 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈)
5 simpl21 1252 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 No )
6 simpl1l 1225 . . . . . . . . . . 11 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝐵)
75, 6sseldd 3984 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 No )
8 nodmon 27695 . . . . . . . . . 10 (𝑈 No → dom 𝑈 ∈ On)
97, 8syl 17 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On)
10 onelon 6409 . . . . . . . . 9 ((dom 𝑈 ∈ On ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
119, 10sylan 580 . . . . . . . 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 769 . . . . . . . . . . . 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 6430 . . . . . . . . . . . . 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 699 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
1918fvresd 6926 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
20 onelon 6409 . . . . . . . . . . . . 13 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
2111, 20sylan 580 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
22 fveq2 6906 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
23 fveq2 6906 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
2422, 23neeq12d 3002 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
2524onnminsb 7819 . . . . . . . . . . . 12 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
2621, 12, 25sylc 65 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
27 df-ne 2941 . . . . . . . . . . . 12 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
2827con2bii 357 . . . . . . . . . . 11 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
2926, 28sylibr 234 . . . . . . . . . 10 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
3019, 29eqtr4d 2780 . . . . . . . . 9 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
3130ralrimiva 3146 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
32 simpr 484 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
3332fvresd 6926 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
34 simplr 769 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈)
35 simpl23 1254 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 No )
367adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
37 sltval2 27701 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No ) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3835, 36, 37syl2an2r 685 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
3934, 38mpbid 232 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
40 necom 2994 . . . . . . . . . . . . 13 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
4140rabbii 3442 . . . . . . . . . . . 12 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4241inteqi 4950 . . . . . . . . . . 11 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
4342fveq2i 6909 . . . . . . . . . 10 (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4442fveq2i 6909 . . . . . . . . . 10 (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})
4539, 43, 443brtr4g 5177 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
4633, 45eqbrtrd 5165 . . . . . . . 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 6906 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
49 fveq2 6906 . . . . . . . . . . 11 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
5048, 49breq12d 5156 . . . . . . . . . 10 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝) ↔ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5147, 50anbi12d 632 . . . . . . . . 9 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
5251rspcev 3622 . . . . . . . 8 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
5311, 31, 46, 52syl12anc 837 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝)))
54 noreson 27705 . . . . . . . . 9 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
5535, 9, 54syl2anc 584 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
56 sltval 27692 . . . . . . . 8 (((𝑍 ↾ dom 𝑈) ∈ No 𝑈 No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈𝑝))))
5755, 36, 56syl2an2r 685 . . . . . . 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 6464 . . . . . . 7 dom 𝑈 ⊆ suc dom 𝑈
60 resabs1 6024 . . . . . . 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 6012 . . . . . . 7 ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈))
63 nofun 27694 . . . . . . . . . . . . 13 (𝑈 No → Fun 𝑈)
647, 63syl 17 . . . . . . . . . . . 12 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈)
65 funrel 6583 . . . . . . . . . . . 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 6044 . . . . . . . . . 10 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
6967, 68syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
70 nodmord 27698 . . . . . . . . . . . . 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 6402 . . . . . . . . . . 11 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
7472, 73syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
75 1oex 8516 . . . . . . . . . . 11 1o ∈ V
7675snres0 6318 . . . . . . . . . 10 (({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
7774, 76sylibr 234 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈) = ∅)
7869, 77uneq12d 4169 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = (𝑈 ∪ ∅))
79 un0 4394 . . . . . . . 8 (𝑈 ∪ ∅) = 𝑈
8078, 79eqtrdi 2793 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 1o⟩} ↾ dom 𝑈)) = 𝑈)
8162, 80eqtrid 2789 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈) = 𝑈)
8258, 61, 813brtr4d 5175 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ↾ dom 𝑈))
83 onsucb 7837 . . . . . . . . 9 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
849, 83sylib 218 . . . . . . . 8 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On)
85 noreson 27705 . . . . . . . 8 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8635, 84, 85syl2anc 584 . . . . . . 7 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8786adantr 480 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
8875prid1 4762 . . . . . . . . 9 1o ∈ {1o, 2o}
8988noextend 27711 . . . . . . . 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 27707 . . . . . 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 1373 . . . . 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 27721 . . . . . 6 <s Or No
96 soasym 5625 . . . . . 6 (( <s Or No ∧ ((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No )) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9795, 96mpan 690 . . . . 5 (((𝑍 ↾ suc dom 𝑈) ∈ No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
9886, 91, 97syl2an2r 685 . . . 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 5616 . . . . . 6 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
10195, 90, 100sylancr 587 . . . . 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 6390 . . . . . . . 8 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
104103reseq2i 5994 . . . . . . 7 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
105 resundi 6011 . . . . . . 7 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
106104, 105eqtri 2765 . . . . . 6 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
107 dmres 6030 . . . . . . . . 9 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
10842eqeq1i 2742 . . . . . . . . . . . . 13 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} = dom 𝑈)
109108biimpi 216 . . . . . . . . . . . 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 1209 . . . . . . . . . . . . . . . . . 18 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → 𝑍 No )
114 sonr 5616 . . . . . . . . . . . . . . . . . 18 (( <s Or No 𝑍 No ) → ¬ 𝑍 <s 𝑍)
11595, 113, 114sylancr 587 . . . . . . . . . . . . . . . . 17 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍)
116 breq2 5147 . . . . . . . . . . . . . . . . . 18 (𝑈 = 𝑍 → (𝑍 <s 𝑈𝑍 <s 𝑍))
117116notbid 318 . . . . . . . . . . . . . . . . 17 (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍))
118115, 117syl5ibrcom 247 . . . . . . . . . . . . . . . 16 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈))
119118necon2ad 2955 . . . . . . . . . . . . . . 15 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈𝑈𝑍))
120119imp 406 . . . . . . . . . . . . . 14 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈𝑍)
121120necomd 2996 . . . . . . . . . . . . 13 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍𝑈)
122121adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
123 nosepssdm 27731 . . . . . . . . . . . 12 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
124111, 112, 122, 123syl3anc 1373 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
125110, 124eqsstrrd 4019 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
126 dfss2 3969 . . . . . . . . . 10 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
127125, 126sylib 218 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
128107, 127eqtrid 2789 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
129128eleq2d 2827 . . . . . . . . . 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 6926 . . . . . . . . . . . 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 6409 . . . . . . . . . . . . . . 15 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
134132, 133sylan 580 . . . . . . . . . . . . . 14 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
135 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
136135eleq2d 2827 . . . . . . . . . . . . . . 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 2997 . . . . . . . . . . . . . 14 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
140139con2bii 357 . . . . . . . . . . . . 13 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
141138, 140sylibr 234 . . . . . . . . . . . 12 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
142131, 141eqtrd 2777 . . . . . . . . . . 11 ((((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
143142ex 412 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
144129, 143sylbid 240 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
145144ralrimiv 3145 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
146 nofun 27694 . . . . . . . . . . 11 (𝑍 No → Fun 𝑍)
147111, 146syl 17 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑍)
148147funresd 6609 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
14964adantr 480 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑈)
150 eqfunfv 7056 . . . . . . . . 9 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
151148, 149, 150syl2anc 584 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
152128, 145, 151mpbir2and 713 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
15335, 146syl 17 . . . . . . . . . 10 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍)
154153funfnd 6597 . . . . . . . . 9 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 Fn dom 𝑍)
155 ndmfv 6941 . . . . . . . . . . . . . . . 16 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
156 2on0 8522 . . . . . . . . . . . . . . . . . . 19 2o ≠ ∅
157156necomi 2995 . . . . . . . . . . . . . . . . . 18 ∅ ≠ 2o
158 neeq1 3003 . . . . . . . . . . . . . . . . . 18 ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
159157, 158mpbiri 258 . . . . . . . . . . . . . . . . 17 ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2o)
160159neneqd 2945 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈) = ∅ → ¬ (𝑈‘dom 𝑈) = 2o)
161155, 160syl 17 . . . . . . . . . . . . . . 15 (¬ dom 𝑈 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑈) = 2o)
162112, 70, 73, 1614syl 19 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 2o)
163162intnand 488 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o))
164 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈)
16535, 7, 37syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)})))
166164, 165mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
167166adantr 480 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}))
168110fveq2d 6910 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑍‘dom 𝑈))
169110fveq2d 6910 . . . . . . . . . . . . . . 15 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}) = (𝑈‘dom 𝑈))
170167, 168, 1693brtr3d 5174 . . . . . . . . . . . . . 14 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈))
171 fvex 6919 . . . . . . . . . . . . . . 15 (𝑍‘dom 𝑈) ∈ V
172 fvex 6919 . . . . . . . . . . . . . . 15 (𝑈‘dom 𝑈) ∈ V
173171, 172brtp 5528 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑈‘dom 𝑈) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
174170, 173sylib 218 . . . . . . . . . . . . 13 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)))
175 3orel3 1488 . . . . . . . . . . . . 13 (¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o) → ((((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o))))
176163, 174, 175sylc 65 . . . . . . . . . . . 12 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))
177 andi 1010 . . . . . . . . . . . 12 (((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))
178176, 177sylibr 234 . . . . . . . . . . 11 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)))
179178simpld 494 . . . . . . . . . 10 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1o)
180 ndmfv 6941 . . . . . . . . . . . 12 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
181 1n0 8526 . . . . . . . . . . . . . . 15 1o ≠ ∅
182181necomi 2995 . . . . . . . . . . . . . 14 ∅ ≠ 1o
183 neeq1 3003 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
184182, 183mpbiri 258 . . . . . . . . . . . . 13 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1o)
185184neneqd 2945 . . . . . . . . . . . 12 ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 1o)
186180, 185syl 17 . . . . . . . . . . 11 (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 1o)
187186con4i 114 . . . . . . . . . 10 ((𝑍‘dom 𝑈) = 1o → dom 𝑈 ∈ dom 𝑍)
188179, 187syl 17 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
189 fnressn 7178 . . . . . . . . 9 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
190154, 188, 189syl2an2r 685 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
191179opeq2d 4880 . . . . . . . . 9 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 1o⟩)
192191sneqd 4638 . . . . . . . 8 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 1o⟩})
193190, 192eqtrd 2777 . . . . . . 7 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 1o⟩})
194152, 193uneq12d 4169 . . . . . 6 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
195106, 194eqtrid 2789 . . . . 5 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 1o⟩}))
196195breq2d 5155 . . . 4 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈) ↔ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 1o⟩})))
197102, 196mtbird 325 . . 3 (((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
198 nosepssdm 27731 . . . . 5 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
1997, 35, 120, 198syl3anc 1373 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
200 nosepon 27710 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
2017, 35, 120, 200syl3anc 1373 . . . . 5 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
202 onsseleq 6425 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
203201, 9, 202syl2anc 584 . . . 4 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
204199, 203mpbid 232 . . 3 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈))
20599, 197, 204mpjaodan 961 . 2 ((((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
2064, 205mpdan 687 1 (((𝑈𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {⟨dom 𝑈, 1o⟩}) <s (𝑍 ↾ suc dom 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3o 1086  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626  {ctp 4630  cop 4632   cint 4946   class class class wbr 5143   Or wor 5591  dom cdm 5685  cres 5687  Rel wrel 5690  Ord word 6383  Oncon0 6384  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  cfv 6561  1oc1o 8499  2oc2o 8500   No csur 27684   <s cslt 27685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-1o 8506  df-2o 8507  df-no 27687  df-slt 27688
This theorem is referenced by:  noinfbnd2  27776
  Copyright terms: Public domain W3C validator