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

Theorem nosupbnd2lem1 33275
 Description: Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021.)
Assertion
Ref Expression
nosupbnd2lem1 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
Distinct variable groups:   𝐴,𝑎   𝑈,𝑎   𝑍,𝑎
Allowed substitution hints:   𝐴(𝑦)   𝑈(𝑦)   𝑍(𝑦)

Proof of Theorem nosupbnd2lem1
Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1l 1194 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈𝐴)
2 simp3 1135 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ∀𝑎𝐴 𝑎 <s 𝑍)
3 breq1 5055 . . . 4 (𝑎 = 𝑈 → (𝑎 <s 𝑍𝑈 <s 𝑍))
43rspcv 3604 . . 3 (𝑈𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑈 <s 𝑍))
51, 2, 4sylc 65 . 2 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍)
6 simpl21 1248 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 No )
7 simpl1l 1221 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝐴)
86, 7sseldd 3954 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 No )
9 simpl23 1250 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 No )
10 simp21 1203 . . . . . . . . . 10 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝐴 No )
1110, 1sseldd 3954 . . . . . . . . 9 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 No )
12 sltso 33241 . . . . . . . . . 10 <s Or No
13 sonr 5483 . . . . . . . . . 10 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
1412, 13mpan 689 . . . . . . . . 9 (𝑈 No → ¬ 𝑈 <s 𝑈)
1511, 14syl 17 . . . . . . . 8 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈)
16 breq2 5056 . . . . . . . . 9 (𝑈 = 𝑍 → (𝑈 <s 𝑈𝑈 <s 𝑍))
1716notbid 321 . . . . . . . 8 (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍))
1815, 17syl5ibcom 248 . . . . . . 7 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍))
1918con2d 136 . . . . . 6 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍))
2019imp 410 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍)
2120neqned 3021 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝑍)
22 nosepssdm 33250 . . . 4 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
238, 9, 21, 22syl3anc 1368 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
24 nosepon 33232 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
258, 9, 21, 24syl3anc 1368 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
26 nodmon 33217 . . . . . 6 (𝑈 No → dom 𝑈 ∈ On)
278, 26syl 17 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On)
28 onsseleq 6219 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
2925, 27, 28syl2anc 587 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
308adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
319adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 No )
3221adantr 484 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈𝑍)
3330, 31, 32, 24syl3anc 1368 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
34 onelon 6203 . . . . . . . . . . . . . . . 16 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
3533, 34sylan 583 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
36 simpr 488 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
37 fveq2 6661 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
38 fveq2 6661 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
3937, 38neeq12d 3075 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
4039onnminsb 7513 . . . . . . . . . . . . . . 15 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
42 df-ne 3015 . . . . . . . . . . . . . . 15 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
4342con2bii 361 . . . . . . . . . . . . . 14 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
4441, 43sylibr 237 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
45 simplr 768 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
4627adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
4746adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
48 ontr1 6224 . . . . . . . . . . . . . . . 16 (dom 𝑈 ∈ On → ((𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
4947, 48syl 17 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈))
5036, 45, 49mp2and 698 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
5150fvresd 6681 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
5244, 51eqtr4d 2862 . . . . . . . . . . . 12 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
5352ralrimiva 3177 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
54 simplr 768 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍)
55 sltval2 33223 . . . . . . . . . . . . . 14 ((𝑈 No 𝑍 No ) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5630, 31, 55syl2anc 587 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5754, 56mpbid 235 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
58 simpr 488 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
5958fvresd 6681 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6057, 59breqtrrd 5080 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
61 raleq 3396 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)))
62 fveq2 6661 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
63 fveq2 6661 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6462, 63breq12d 5065 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
6561, 64anbi12d 633 . . . . . . . . . . . 12 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
6665rspcev 3609 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
6733, 53, 60, 66syl12anc 835 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
68 noreson 33227 . . . . . . . . . . . 12 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
6931, 46, 68syl2anc 587 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
70 sltval 33214 . . . . . . . . . . 11 ((𝑈 No ∧ (𝑍 ↾ dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7130, 69, 70syl2anc 587 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7267, 71mpbird 260 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈))
73 df-res 5554 . . . . . . . . . . . . 13 ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈) = ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V))
74 2on 8107 . . . . . . . . . . . . . . . 16 2o ∈ On
75 xpsng 6892 . . . . . . . . . . . . . . . 16 ((dom 𝑈 ∈ On ∧ 2o ∈ On) → ({dom 𝑈} × {2o}) = {⟨dom 𝑈, 2o⟩})
7646, 74, 75sylancl 589 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2o}) = {⟨dom 𝑈, 2o⟩})
7776ineq1d 4173 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) = ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V)))
78 incom 4163 . . . . . . . . . . . . . . . 16 ({dom 𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈})
79 nodmord 33220 . . . . . . . . . . . . . . . . . 18 (𝑈 No → Ord dom 𝑈)
80 ordirr 6196 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
82 disjsn 4632 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
8381, 82sylibr 237 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅)
8478, 83syl5eq 2871 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅)
85 xpdisj1 6005 . . . . . . . . . . . . . . 15 (({dom 𝑈} ∩ dom 𝑈) = ∅ → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) = ∅)
8684, 85syl 17 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) = ∅)
8777, 86eqtr3d 2861 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V)) = ∅)
8873, 87syl5eq 2871 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈) = ∅)
8988uneq2d 4125 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅))
90 resundir 5855 . . . . . . . . . . 11 ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈))
91 un0 4327 . . . . . . . . . . . 12 ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈)
9291eqcomi 2833 . . . . . . . . . . 11 (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅)
9389, 90, 923eqtr4g 2884 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈))
94 nofun 33216 . . . . . . . . . . . 12 (𝑈 No → Fun 𝑈)
9530, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Fun 𝑈)
96 funrel 6360 . . . . . . . . . . 11 (Fun 𝑈 → Rel 𝑈)
97 resdm 5884 . . . . . . . . . . 11 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
9895, 96, 973syl 18 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
9993, 98eqtrd 2859 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = 𝑈)
100 sssucid 6255 . . . . . . . . . 10 dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 5870 . . . . . . . . . 10 (dom 𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
102100, 101mp1i 13 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈))
10372, 99, 1023brtr4d 5084 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈))
10474elexi 3499 . . . . . . . . . . . . 13 2o ∈ V
105104prid2 4684 . . . . . . . . . . . 12 2o ∈ {1o, 2o}
106105noextend 33233 . . . . . . . . . . 11 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
1078, 106syl 17 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
108107adantr 484 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
109 sucelon 7526 . . . . . . . . . . . 12 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
11027, 109sylib 221 . . . . . . . . . . 11 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On)
111 noreson 33227 . . . . . . . . . . 11 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
1129, 110, 111syl2anc 587 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No )
113112adantr 484 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
114 sltres 33229 . . . . . . . . 9 (((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ∧ dom 𝑈 ∈ On) → (((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
115108, 113, 46, 114syl3anc 1368 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈)))
116103, 115mpd 15 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈))
117 soasym 5491 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
11812, 117mpan 689 . . . . . . . 8 (((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
119108, 113, 118syl2anc 587 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
120116, 119mpd 15 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
121 df-suc 6184 . . . . . . . . . 10 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
122121reseq2i 5837 . . . . . . . . 9 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
123 resundi 5854 . . . . . . . . 9 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
124122, 123eqtri 2847 . . . . . . . 8 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
125 dmres 5862 . . . . . . . . . . 11 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
126 simpr 488 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
127 necom 3067 . . . . . . . . . . . . . . . 16 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
128127rabbii 3458 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
129128inteqi 4866 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
1309adantr 484 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1318adantr 484 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
13221adantr 484 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈𝑍)
133132necomd 3069 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
134 nosepssdm 33250 . . . . . . . . . . . . . . 15 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
135130, 131, 133, 134syl3anc 1368 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
136129, 135eqsstrid 4001 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑍)
137126, 136eqsstrrd 3992 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
138 df-ss 3936 . . . . . . . . . . . 12 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
139137, 138sylib 221 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
140125, 139syl5eq 2871 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
141140eleq2d 2901 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
142 simpr 488 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
143142fvresd 6681 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
144131, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ On)
145 onelon 6203 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
146144, 145sylan 583 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
147126eleq2d 2901 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
148147biimpar 481 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
149146, 148, 40sylc 65 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
150 nesym 3070 . . . . . . . . . . . . . . . 16 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
151150con2bii 361 . . . . . . . . . . . . . . 15 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
152149, 151sylibr 237 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
153143, 152eqtrd 2859 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
154153ex 416 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
155141, 154sylbid 243 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
156155ralrimiv 3176 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
157 nofun 33216 . . . . . . . . . . . 12 (𝑍 No → Fun 𝑍)
158 funres 6385 . . . . . . . . . . . 12 (Fun 𝑍 → Fun (𝑍 ↾ dom 𝑈))
159130, 157, 1583syl 18 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈))
160131, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑈)
161 eqfunfv 6798 . . . . . . . . . . 11 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
162159, 160, 161syl2anc 587 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
163140, 156, 162mpbir2and 712 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈)
164130, 157syl 17 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Fun 𝑍)
165 funfn 6373 . . . . . . . . . . . 12 (Fun 𝑍𝑍 Fn dom 𝑍)
166164, 165sylib 221 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍)
167 1oex 8106 . . . . . . . . . . . . . . . . . . 19 1o ∈ V
168167prid1 4683 . . . . . . . . . . . . . . . . . 18 1o ∈ {1o, 2o}
169168nosgnn0i 33226 . . . . . . . . . . . . . . . . 17 ∅ ≠ 1o
170131, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
171 ndmfv 6691 . . . . . . . . . . . . . . . . . . 19 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
172170, 80, 1713syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅)
173172neeq1d 3073 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
174169, 173mpbiri 261 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠ 1o)
175174neneqd 3019 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1o)
176175intnanrd 493 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅))
177175intnanrd 493 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o))
178 simplr 768 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 <s 𝑍)
179131, 130, 55syl2anc 587 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
180178, 179mpbid 235 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
181 fveq2 6661 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
182181adantl 485 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
183 fveq2 6661 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
184183adantl 485 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
185180, 182, 1843brtr3d 5083 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈))
186 fvex 6674 . . . . . . . . . . . . . . . . 17 (𝑈‘dom 𝑈) ∈ V
187 fvex 6674 . . . . . . . . . . . . . . . . 17 (𝑍‘dom 𝑈) ∈ V
188186, 187brtp 33045 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)))
189 3orrot 1089 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)))
190 3orrot 1089 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
191188, 189, 1903bitri 300 . . . . . . . . . . . . . . 15 ((𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
192185, 191sylib 221 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
193176, 177, 192ecase23d 1470 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o))
194193simprd 499 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2o)
195 ndmfv 6691 . . . . . . . . . . . . . 14 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
196105nosgnn0i 33226 . . . . . . . . . . . . . . . 16 ∅ ≠ 2o
197 neeq1 3076 . . . . . . . . . . . . . . . 16 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
198196, 197mpbiri 261 . . . . . . . . . . . . . . 15 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2o)
199198neneqd 3019 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 2o)
200195, 199syl 17 . . . . . . . . . . . . 13 (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 2o)
201200con4i 114 . . . . . . . . . . . 12 ((𝑍‘dom 𝑈) = 2o → dom 𝑈 ∈ dom 𝑍)
202194, 201syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
203 fnressn 6911 . . . . . . . . . . 11 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
204166, 202, 203syl2anc 587 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
205194opeq2d 4796 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 2o⟩)
206205sneqd 4562 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 2o⟩})
207204, 206eqtrd 2859 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 2o⟩})
208163, 207uneq12d 4126 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
209124, 208syl5eq 2871 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
210 sonr 5483 . . . . . . . . 9 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
21112, 210mpan 689 . . . . . . . 8 ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No → ¬ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
212131, 106, 2113syl 18 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
213209, 212eqnbrtrd 5070 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
214120, 213jaodan 955 . . . . 5 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
215214ex 416 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
21629, 215sylbid 243 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
21723, 216mpd 15 . 2 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
2185, 217mpdan 686 1 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
 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 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  {crab 3137  Vcvv 3480   ∪ cun 3917   ∩ cin 3918   ⊆ wss 3919  ∅c0 4276  {csn 4550  {ctp 4554  ⟨cop 4556  ∩ cint 4862   class class class wbr 5052   Or wor 5460   × cxp 5540  dom cdm 5542   ↾ cres 5544  Rel wrel 5547  Ord word 6177  Oncon0 6178  suc csuc 6180  Fun wfun 6337   Fn wfn 6338  ‘cfv 6343  1oc1o 8091  2oc2o 8092   No csur 33207
 Copyright terms: Public domain W3C validator