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

Theorem nosupbnd2lem1 32138
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 𝑈, 2𝑜⟩}))
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 1216 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈𝐴)
2 simp3 1130 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ∀𝑎𝐴 𝑎 <s 𝑍)
3 breq1 4795 . . . 4 (𝑎 = 𝑈 → (𝑎 <s 𝑍𝑈 <s 𝑍))
43rspcv 3433 . . 3 (𝑈𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑈 <s 𝑍))
51, 2, 4sylc 65 . 2 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍)
6 simpl21 1297 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 No )
7 simpl1l 1255 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝐴)
86, 7sseldd 3733 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 No )
9 simpl23 1301 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 No )
10 simp21 1225 . . . . . . . . . 10 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝐴 No )
1110, 1sseldd 3733 . . . . . . . . 9 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 No )
12 sltso 32104 . . . . . . . . . 10 <s Or No
13 sonr 5196 . . . . . . . . . 10 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
1412, 13mpan 708 . . . . . . . . 9 (𝑈 No → ¬ 𝑈 <s 𝑈)
1511, 14syl 17 . . . . . . . 8 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈)
16 breq2 4796 . . . . . . . . 9 (𝑈 = 𝑍 → (𝑈 <s 𝑈𝑈 <s 𝑍))
1716notbid 307 . . . . . . . 8 (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍))
1815, 17syl5ibcom 235 . . . . . . 7 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍))
1918con2d 129 . . . . . 6 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍))
2019imp 444 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍)
2120neqned 2927 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝑍)
22 nosepssdm 32113 . . . 4 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
238, 9, 21, 22syl3anc 1463 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
24 nosepon 32095 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
258, 9, 21, 24syl3anc 1463 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
26 nodmon 32080 . . . . . 6 (𝑈 No → dom 𝑈 ∈ On)
278, 26syl 17 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On)
28 onsseleq 5914 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
2925, 27, 28syl2anc 696 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
308adantr 472 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
319adantr 472 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 No )
3221adantr 472 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈𝑍)
3330, 31, 32, 24syl3anc 1463 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
34 onelon 5897 . . . . . . . . . . . . . . . 16 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
3533, 34sylan 489 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
36 simpr 479 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
37 fveq2 6340 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
38 fveq2 6340 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
3937, 38neeq12d 2981 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
4039onnminsb 7157 . . . . . . . . . . . . . . 15 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
42 df-ne 2921 . . . . . . . . . . . . . . 15 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
4342con2bii 346 . . . . . . . . . . . . . 14 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
4441, 43sylibr 224 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
45 simplr 809 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
4627adantr 472 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
4746adantr 472 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
48 ontr1 5920 . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
5150fvresd 6357 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
5244, 51eqtr4d 2785 . . . . . . . . . . . 12 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
5352ralrimiva 3092 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
54 simplr 809 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍)
55 sltval2 32086 . . . . . . . . . . . . . 14 ((𝑈 No 𝑍 No ) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5630, 31, 55syl2anc 696 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5754, 56mpbid 222 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
58 simpr 479 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
5958fvresd 6357 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6057, 59breqtrrd 4820 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
61 raleq 3265 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)))
62 fveq2 6340 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
63 fveq2 6340 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6462, 63breq12d 4805 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
6561, 64anbi12d 749 . . . . . . . . . . . 12 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
6665rspcev 3437 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
6733, 53, 60, 66syl12anc 1461 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
68 noreson 32090 . . . . . . . . . . . 12 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
6931, 46, 68syl2anc 696 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
70 sltval 32077 . . . . . . . . . . 11 ((𝑈 No ∧ (𝑍 ↾ dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7130, 69, 70syl2anc 696 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7267, 71mpbird 247 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈))
73 df-res 5266 . . . . . . . . . . . . 13 ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V))
74 2on 7725 . . . . . . . . . . . . . . . 16 2𝑜 ∈ On
75 xpsng 6557 . . . . . . . . . . . . . . . 16 ((dom 𝑈 ∈ On ∧ 2𝑜 ∈ On) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7646, 74, 75sylancl 697 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7776ineq1d 3944 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩ (dom 𝑈 × V)) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)))
78 incom 3936 . . . . . . . . . . . . . . . 16 ({dom 𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈})
79 nodmord 32083 . . . . . . . . . . . . . . . . . 18 (𝑈 No → Ord dom 𝑈)
80 ordirr 5890 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
82 disjsn 4378 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅)
8478, 83syl5eq 2794 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅)
85 xpdisj1 5701 . . . . . . . . . . . . . . 15 (({dom 𝑈} ∩ dom 𝑈) = ∅ → (({dom 𝑈} × {2𝑜}) ∩ (dom 𝑈 × V)) = ∅)
8684, 85syl 17 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩ (dom 𝑈 × V)) = ∅)
8777, 86eqtr3d 2784 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)) = ∅)
8873, 87syl5eq 2794 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ∅)
8988uneq2d 3898 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅))
90 resundir 5557 . . . . . . . . . . 11 ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈))
91 un0 4098 . . . . . . . . . . . 12 ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈)
9291eqcomi 2757 . . . . . . . . . . 11 (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅)
9389, 90, 923eqtr4g 2807 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈))
94 nofun 32079 . . . . . . . . . . . 12 (𝑈 No → Fun 𝑈)
9530, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Fun 𝑈)
96 funrel 6054 . . . . . . . . . . 11 (Fun 𝑈 → Rel 𝑈)
97 resdm 5587 . . . . . . . . . . 11 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
9895, 96, 973syl 18 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
9993, 98eqtrd 2782 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = 𝑈)
100 sssucid 5951 . . . . . . . . . 10 dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 5573 . . . . . . . . . 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 4824 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈))
10474elexi 3341 . . . . . . . . . . . . 13 2𝑜 ∈ V
105104prid2 4430 . . . . . . . . . . . 12 2𝑜 ∈ {1𝑜, 2𝑜}
106105noextend 32096 . . . . . . . . . . 11 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
1078, 106syl 17 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
108107adantr 472 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
109 sucelon 7170 . . . . . . . . . . . 12 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
11027, 109sylib 208 . . . . . . . . . . 11 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On)
111 noreson 32090 . . . . . . . . . . 11 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
1129, 110, 111syl2anc 696 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No )
113112adantr 472 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
114 sltres 32092 . . . . . . . . 9 (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ∧ dom 𝑈 ∈ On) → (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈)))
115108, 113, 46, 114syl3anc 1463 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈)))
116103, 115mpd 15 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈))
117 soasym 31935 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
11812, 117mpan 708 . . . . . . . 8 (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
119108, 113, 118syl2anc 696 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
120116, 119mpd 15 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
121 df-suc 5878 . . . . . . . . . 10 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
122121reseq2i 5536 . . . . . . . . 9 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
123 resundi 5556 . . . . . . . . 9 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
124122, 123eqtri 2770 . . . . . . . 8 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
125 dmres 5565 . . . . . . . . . . 11 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
126 simpr 479 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
127 necom 2973 . . . . . . . . . . . . . . . 16 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
128127rabbii 3313 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
129128inteqi 4619 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
1309adantr 472 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1318adantr 472 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
13221adantr 472 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈𝑍)
133132necomd 2975 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
134 nosepssdm 32113 . . . . . . . . . . . . . . 15 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
135130, 131, 133, 134syl3anc 1463 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
136129, 135syl5eqss 3778 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑍)
137126, 136eqsstr3d 3769 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
138 df-ss 3717 . . . . . . . . . . . 12 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
139137, 138sylib 208 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
140125, 139syl5eq 2794 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
141140eleq2d 2813 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
142 simpr 479 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
143142fvresd 6357 . . . . . . . . . . . . . 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 5897 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
146144, 145sylan 489 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
147126eleq2d 2813 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
148147biimpar 503 . . . . . . . . . . . . . . . 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 2976 . . . . . . . . . . . . . . . 16 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
151150con2bii 346 . . . . . . . . . . . . . . 15 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
152149, 151sylibr 224 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
153143, 152eqtrd 2782 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
154153ex 449 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
155141, 154sylbid 230 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
156155ralrimiv 3091 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
157 nofun 32079 . . . . . . . . . . . 12 (𝑍 No → Fun 𝑍)
158 funres 6078 . . . . . . . . . . . 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 6467 . . . . . . . . . . 11 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
162159, 160, 161syl2anc 696 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
163140, 156, 162mpbir2and 995 . . . . . . . . 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 6067 . . . . . . . . . . . 12 (Fun 𝑍𝑍 Fn dom 𝑍)
166164, 165sylib 208 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍)
167 1on 7724 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ On
168167elexi 3341 . . . . . . . . . . . . . . . . . . 19 1𝑜 ∈ V
169168prid1 4429 . . . . . . . . . . . . . . . . . 18 1𝑜 ∈ {1𝑜, 2𝑜}
170169nosgnn0i 32089 . . . . . . . . . . . . . . . . 17 ∅ ≠ 1𝑜
171131, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
172 ndmfv 6367 . . . . . . . . . . . . . . . . . . 19 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
173171, 80, 1723syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅)
174173neeq1d 2979 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1𝑜 ↔ ∅ ≠ 1𝑜))
175170, 174mpbiri 248 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠ 1𝑜)
176175neneqd 2925 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1𝑜)
177176intnanrd 1001 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅))
178176intnanrd 1001 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜))
179 simplr 809 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 <s 𝑍)
180131, 130, 55syl2anc 696 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
181179, 180mpbid 222 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
182 fveq2 6340 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
183182adantl 473 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
184 fveq2 6340 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
185184adantl 473 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
186181, 183, 1853brtr3d 4823 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈))
187 fvex 6350 . . . . . . . . . . . . . . . . 17 (𝑈‘dom 𝑈) ∈ V
188 fvex 6350 . . . . . . . . . . . . . . . . 17 (𝑍‘dom 𝑈) ∈ V
189187, 188brtp 31917 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)))
190 3orrot 1077 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)))
191 3orrot 1077 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
192189, 190, 1913bitri 286 . . . . . . . . . . . . . . 15 ((𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
193186, 192sylib 208 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
194177, 178, 193ecase23d 1573 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜))
195194simprd 482 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2𝑜)
196 ndmfv 6367 . . . . . . . . . . . . . 14 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
197105nosgnn0i 32089 . . . . . . . . . . . . . . . 16 ∅ ≠ 2𝑜
198 neeq1 2982 . . . . . . . . . . . . . . . 16 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2𝑜 ↔ ∅ ≠ 2𝑜))
199197, 198mpbiri 248 . . . . . . . . . . . . . . 15 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2𝑜)
200199neneqd 2925 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 2𝑜)
201196, 200syl 17 . . . . . . . . . . . . 13 (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 2𝑜)
202201con4i 113 . . . . . . . . . . . 12 ((𝑍‘dom 𝑈) = 2𝑜 → dom 𝑈 ∈ dom 𝑍)
203195, 202syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
204 fnressn 6576 . . . . . . . . . . 11 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
205166, 203, 204syl2anc 696 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
206195opeq2d 4548 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 2𝑜⟩)
207206sneqd 4321 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 2𝑜⟩})
208205, 207eqtrd 2782 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 2𝑜⟩})
209163, 208uneq12d 3899 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
210124, 209syl5eq 2794 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
211 sonr 5196 . . . . . . . . 9 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
21212, 211mpan 708 . . . . . . . 8 ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
213131, 106, 2123syl 18 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
214210, 213eqnbrtrd 4810 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
215120, 214jaodan 861 . . . . 5 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
216215ex 449 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
21729, 216sylbid 230 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
21823, 217mpd 15 . 2 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
2195, 218mpdan 705 1 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1071  w3a 1072   = wceq 1620  wcel 2127  wne 2920  wral 3038  wrex 3039  {crab 3042  Vcvv 3328  cun 3701  cin 3702  wss 3703  c0 4046  {csn 4309  {ctp 4313  cop 4315   cint 4615   class class class wbr 4792   Or wor 5174   × cxp 5252  dom cdm 5254  cres 5256  Rel wrel 5259  Ord word 5871  Oncon0 5872  suc csuc 5874  Fun wfun 6031   Fn wfn 6032  cfv 6037  1𝑜c1o 7710  2𝑜c2o 7711   No csur 32070   <s cslt 32071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-ord 5875  df-on 5876  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-1o 7717  df-2o 7718  df-no 32073  df-slt 32074
This theorem is referenced by:  nosupbnd2  32139
  Copyright terms: Public domain W3C validator