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 32176
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 1247 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈𝐴)
2 simp3 1161 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ∀𝑎𝐴 𝑎 <s 𝑍)
3 breq1 4840 . . . 4 (𝑎 = 𝑈 → (𝑎 <s 𝑍𝑈 <s 𝑍))
43rspcv 3494 . . 3 (𝑈𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑈 <s 𝑍))
51, 2, 4sylc 65 . 2 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍)
6 simpl21 1328 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 No )
7 simpl1l 1286 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝐴)
86, 7sseldd 3793 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 No )
9 simpl23 1332 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 No )
10 simp21 1256 . . . . . . . . . 10 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝐴 No )
1110, 1sseldd 3793 . . . . . . . . 9 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 No )
12 sltso 32142 . . . . . . . . . 10 <s Or No
13 sonr 5247 . . . . . . . . . 10 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
1412, 13mpan 673 . . . . . . . . 9 (𝑈 No → ¬ 𝑈 <s 𝑈)
1511, 14syl 17 . . . . . . . 8 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈)
16 breq2 4841 . . . . . . . . 9 (𝑈 = 𝑍 → (𝑈 <s 𝑈𝑈 <s 𝑍))
1716notbid 309 . . . . . . . 8 (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍))
1815, 17syl5ibcom 236 . . . . . . 7 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍))
1918con2d 131 . . . . . 6 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍))
2019imp 395 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍)
2120neqned 2981 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝑍)
22 nosepssdm 32151 . . . 4 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
238, 9, 21, 22syl3anc 1483 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
24 nosepon 32133 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
258, 9, 21, 24syl3anc 1483 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
26 nodmon 32118 . . . . . 6 (𝑈 No → dom 𝑈 ∈ On)
278, 26syl 17 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On)
28 onsseleq 5972 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
2925, 27, 28syl2anc 575 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
308adantr 468 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
319adantr 468 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 No )
3221adantr 468 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈𝑍)
3330, 31, 32, 24syl3anc 1483 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
34 onelon 5955 . . . . . . . . . . . . . . . 16 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
3533, 34sylan 571 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
36 simpr 473 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
37 fveq2 6402 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
38 fveq2 6402 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
3937, 38neeq12d 3035 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
4039onnminsb 7228 . . . . . . . . . . . . . . 15 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
42 df-ne 2975 . . . . . . . . . . . . . . 15 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
4342con2bii 348 . . . . . . . . . . . . . 14 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
4441, 43sylibr 225 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
45 simplr 776 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
4627adantr 468 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
4746adantr 468 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
48 ontr1 5978 . . . . . . . . . . . . . . . 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 682 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
5150fvresd 6422 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
5244, 51eqtr4d 2839 . . . . . . . . . . . 12 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
5352ralrimiva 3150 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
54 simplr 776 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍)
55 sltval2 32124 . . . . . . . . . . . . . 14 ((𝑈 No 𝑍 No ) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5630, 31, 55syl2anc 575 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5754, 56mpbid 223 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
58 simpr 473 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
5958fvresd 6422 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6057, 59breqtrrd 4865 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
61 raleq 3323 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)))
62 fveq2 6402 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
63 fveq2 6402 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6462, 63breq12d 4850 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
6561, 64anbi12d 618 . . . . . . . . . . . 12 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
6665rspcev 3498 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
6733, 53, 60, 66syl12anc 856 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
68 noreson 32128 . . . . . . . . . . . 12 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
6931, 46, 68syl2anc 575 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
70 sltval 32115 . . . . . . . . . . 11 ((𝑈 No ∧ (𝑍 ↾ dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7130, 69, 70syl2anc 575 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7267, 71mpbird 248 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈))
73 df-res 5317 . . . . . . . . . . . . 13 ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V))
74 2on 7799 . . . . . . . . . . . . . . . 16 2𝑜 ∈ On
75 xpsng 6623 . . . . . . . . . . . . . . . 16 ((dom 𝑈 ∈ On ∧ 2𝑜 ∈ On) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7646, 74, 75sylancl 576 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7776ineq1d 4006 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩ (dom 𝑈 × V)) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)))
78 incom 3998 . . . . . . . . . . . . . . . 16 ({dom 𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈})
79 nodmord 32121 . . . . . . . . . . . . . . . . . 18 (𝑈 No → Ord dom 𝑈)
80 ordirr 5948 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
82 disjsn 4432 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
8381, 82sylibr 225 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅)
8478, 83syl5eq 2848 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅)
85 xpdisj1 5760 . . . . . . . . . . . . . . 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 2838 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)) = ∅)
8873, 87syl5eq 2848 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ∅)
8988uneq2d 3960 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅))
90 resundir 5609 . . . . . . . . . . 11 ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈))
91 un0 4159 . . . . . . . . . . . 12 ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈)
9291eqcomi 2811 . . . . . . . . . . 11 (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅)
9389, 90, 923eqtr4g 2861 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈))
94 nofun 32117 . . . . . . . . . . . 12 (𝑈 No → Fun 𝑈)
9530, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Fun 𝑈)
96 funrel 6112 . . . . . . . . . . 11 (Fun 𝑈 → Rel 𝑈)
97 resdm 5640 . . . . . . . . . . 11 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
9895, 96, 973syl 18 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
9993, 98eqtrd 2836 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = 𝑈)
100 sssucid 6009 . . . . . . . . . 10 dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 5624 . . . . . . . . . 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 4869 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈))
10474elexi 3403 . . . . . . . . . . . . 13 2𝑜 ∈ V
105104prid2 4483 . . . . . . . . . . . 12 2𝑜 ∈ {1𝑜, 2𝑜}
106105noextend 32134 . . . . . . . . . . 11 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
1078, 106syl 17 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
108107adantr 468 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
109 sucelon 7241 . . . . . . . . . . . 12 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
11027, 109sylib 209 . . . . . . . . . . 11 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On)
111 noreson 32128 . . . . . . . . . . 11 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
1129, 110, 111syl2anc 575 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No )
113112adantr 468 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
114 sltres 32130 . . . . . . . . 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 1483 . . . . . . . 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 31973 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
11812, 117mpan 673 . . . . . . . 8 (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
119108, 113, 118syl2anc 575 . . . . . . 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 5936 . . . . . . . . . 10 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
122121reseq2i 5588 . . . . . . . . 9 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
123 resundi 5608 . . . . . . . . 9 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
124122, 123eqtri 2824 . . . . . . . 8 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
125 dmres 5616 . . . . . . . . . . 11 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
126 simpr 473 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
127 necom 3027 . . . . . . . . . . . . . . . 16 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
128127rabbii 3371 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
129128inteqi 4666 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
1309adantr 468 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1318adantr 468 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
13221adantr 468 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈𝑍)
133132necomd 3029 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
134 nosepssdm 32151 . . . . . . . . . . . . . . 15 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
135130, 131, 133, 134syl3anc 1483 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
136129, 135syl5eqss 3840 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑍)
137126, 136eqsstr3d 3831 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
138 df-ss 3777 . . . . . . . . . . . 12 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
139137, 138sylib 209 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
140125, 139syl5eq 2848 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
141140eleq2d 2867 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
142 simpr 473 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
143142fvresd 6422 . . . . . . . . . . . . . 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 5955 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
146144, 145sylan 571 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
147126eleq2d 2867 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
148147biimpar 465 . . . . . . . . . . . . . . . 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 3030 . . . . . . . . . . . . . . . 16 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
151150con2bii 348 . . . . . . . . . . . . . . 15 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
152149, 151sylibr 225 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
153143, 152eqtrd 2836 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
154153ex 399 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
155141, 154sylbid 231 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
156155ralrimiv 3149 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
157 nofun 32117 . . . . . . . . . . . 12 (𝑍 No → Fun 𝑍)
158 funres 6137 . . . . . . . . . . . 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 6532 . . . . . . . . . . 11 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
162159, 160, 161syl2anc 575 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
163140, 156, 162mpbir2and 695 . . . . . . . . 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 6125 . . . . . . . . . . . 12 (Fun 𝑍𝑍 Fn dom 𝑍)
166164, 165sylib 209 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍)
167 1oex 7798 . . . . . . . . . . . . . . . . . . 19 1𝑜 ∈ V
168167prid1 4482 . . . . . . . . . . . . . . . . . 18 1𝑜 ∈ {1𝑜, 2𝑜}
169168nosgnn0i 32127 . . . . . . . . . . . . . . . . 17 ∅ ≠ 1𝑜
170131, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
171 ndmfv 6432 . . . . . . . . . . . . . . . . . . 19 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
172170, 80, 1713syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅)
173172neeq1d 3033 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1𝑜 ↔ ∅ ≠ 1𝑜))
174169, 173mpbiri 249 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠ 1𝑜)
175174neneqd 2979 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1𝑜)
176175intnanrd 479 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅))
177175intnanrd 479 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜))
178 simplr 776 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 <s 𝑍)
179131, 130, 55syl2anc 575 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
180178, 179mpbid 223 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
181 fveq2 6402 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
182181adantl 469 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
183 fveq2 6402 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
184183adantl 469 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
185180, 182, 1843brtr3d 4868 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈))
186 fvex 6415 . . . . . . . . . . . . . . . . 17 (𝑈‘dom 𝑈) ∈ V
187 fvex 6415 . . . . . . . . . . . . . . . . 17 (𝑍‘dom 𝑈) ∈ V
188186, 187brtp 31955 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)))
189 3orrot 1105 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)))
190 3orrot 1105 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
191188, 189, 1903bitri 288 . . . . . . . . . . . . . . 15 ((𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
192185, 191sylib 209 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)))
193176, 177, 192ecase23d 1590 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜))
194193simprd 485 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2𝑜)
195 ndmfv 6432 . . . . . . . . . . . . . 14 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
196105nosgnn0i 32127 . . . . . . . . . . . . . . . 16 ∅ ≠ 2𝑜
197 neeq1 3036 . . . . . . . . . . . . . . . 16 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2𝑜 ↔ ∅ ≠ 2𝑜))
198196, 197mpbiri 249 . . . . . . . . . . . . . . 15 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2𝑜)
199198neneqd 2979 . . . . . . . . . . . . . 14 ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 2𝑜)
200195, 199syl 17 . . . . . . . . . . . . 13 (¬ dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 2𝑜)
201200con4i 114 . . . . . . . . . . . 12 ((𝑍‘dom 𝑈) = 2𝑜 → dom 𝑈 ∈ dom 𝑍)
202194, 201syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍)
203 fnressn 6643 . . . . . . . . . . 11 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
204166, 202, 203syl2anc 575 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
205194opeq2d 4595 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 2𝑜⟩)
206205sneqd 4376 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 2𝑜⟩})
207204, 206eqtrd 2836 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 2𝑜⟩})
208163, 207uneq12d 3961 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
209124, 208syl5eq 2848 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
210 sonr 5247 . . . . . . . . 9 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
21112, 210mpan 673 . . . . . . . 8 ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
212131, 106, 2113syl 18 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
213209, 212eqnbrtrd 4855 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
214120, 213jaodan 971 . . . . 5 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
215214ex 399 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
21629, 215sylbid 231 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
21723, 216mpd 15 . 2 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
2185, 217mpdan 670 1 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3o 1099  w3a 1100   = wceq 1637  wcel 2155  wne 2974  wral 3092  wrex 3093  {crab 3096  Vcvv 3387  cun 3761  cin 3762  wss 3763  c0 4110  {csn 4364  {ctp 4368  cop 4370   cint 4662   class class class wbr 4837   Or wor 5225   × cxp 5303  dom cdm 5305  cres 5307  Rel wrel 5310  Ord word 5929  Oncon0 5930  suc csuc 5932  Fun wfun 6089   Fn wfn 6090  cfv 6095  1𝑜c1o 7783  2𝑜c2o 7784   No csur 32108   <s cslt 32109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-ord 5933  df-on 5934  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-1o 7790  df-2o 7791  df-no 32111  df-slt 32112
This theorem is referenced by:  nosupbnd2  32177
  Copyright terms: Public domain W3C validator