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 33112
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 1189 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈𝐴)
2 simp3 1130 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ∀𝑎𝐴 𝑎 <s 𝑍)
3 breq1 5060 . . . 4 (𝑎 = 𝑈 → (𝑎 <s 𝑍𝑈 <s 𝑍))
43rspcv 3615 . . 3 (𝑈𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑈 <s 𝑍))
51, 2, 4sylc 65 . 2 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍)
6 simpl21 1243 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 No )
7 simpl1l 1216 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝐴)
86, 7sseldd 3965 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 No )
9 simpl23 1245 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 No )
10 simp21 1198 . . . . . . . . . 10 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝐴 No )
1110, 1sseldd 3965 . . . . . . . . 9 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 No )
12 sltso 33078 . . . . . . . . . 10 <s Or No
13 sonr 5489 . . . . . . . . . 10 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
1412, 13mpan 686 . . . . . . . . 9 (𝑈 No → ¬ 𝑈 <s 𝑈)
1511, 14syl 17 . . . . . . . 8 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈)
16 breq2 5061 . . . . . . . . 9 (𝑈 = 𝑍 → (𝑈 <s 𝑈𝑈 <s 𝑍))
1716notbid 319 . . . . . . . 8 (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍))
1815, 17syl5ibcom 246 . . . . . . 7 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍))
1918con2d 136 . . . . . 6 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍))
2019imp 407 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍)
2120neqned 3020 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝑍)
22 nosepssdm 33087 . . . 4 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
238, 9, 21, 22syl3anc 1363 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
24 nosepon 33069 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
258, 9, 21, 24syl3anc 1363 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
26 nodmon 33054 . . . . . 6 (𝑈 No → dom 𝑈 ∈ On)
278, 26syl 17 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On)
28 onsseleq 6225 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
2925, 27, 28syl2anc 584 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
308adantr 481 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
319adantr 481 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 No )
3221adantr 481 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈𝑍)
3330, 31, 32, 24syl3anc 1363 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
34 onelon 6209 . . . . . . . . . . . . . . . 16 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
3533, 34sylan 580 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
36 simpr 485 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
37 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
38 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
3937, 38neeq12d 3074 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
4039onnminsb 7508 . . . . . . . . . . . . . . 15 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
42 df-ne 3014 . . . . . . . . . . . . . . 15 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
4342con2bii 359 . . . . . . . . . . . . . 14 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
4441, 43sylibr 235 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
45 simplr 765 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
4627adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
4746adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
48 ontr1 6230 . . . . . . . . . . . . . . . 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 695 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
5150fvresd 6683 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
5244, 51eqtr4d 2856 . . . . . . . . . . . 12 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
5352ralrimiva 3179 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
54 simplr 765 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍)
55 sltval2 33060 . . . . . . . . . . . . . 14 ((𝑈 No 𝑍 No ) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5630, 31, 55syl2anc 584 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5754, 56mpbid 233 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
58 simpr 485 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
5958fvresd 6683 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6057, 59breqtrrd 5085 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
61 raleq 3403 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)))
62 fveq2 6663 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
63 fveq2 6663 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6462, 63breq12d 5070 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
6561, 64anbi12d 630 . . . . . . . . . . . 12 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
6665rspcev 3620 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
6733, 53, 60, 66syl12anc 832 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
68 noreson 33064 . . . . . . . . . . . 12 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
6931, 46, 68syl2anc 584 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
70 sltval 33051 . . . . . . . . . . 11 ((𝑈 No ∧ (𝑍 ↾ dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7130, 69, 70syl2anc 584 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7267, 71mpbird 258 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈))
73 df-res 5560 . . . . . . . . . . . . 13 ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈) = ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V))
74 2on 8100 . . . . . . . . . . . . . . . 16 2o ∈ On
75 xpsng 6893 . . . . . . . . . . . . . . . 16 ((dom 𝑈 ∈ On ∧ 2o ∈ On) → ({dom 𝑈} × {2o}) = {⟨dom 𝑈, 2o⟩})
7646, 74, 75sylancl 586 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2o}) = {⟨dom 𝑈, 2o⟩})
7776ineq1d 4185 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) = ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V)))
78 incom 4175 . . . . . . . . . . . . . . . 16 ({dom 𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈})
79 nodmord 33057 . . . . . . . . . . . . . . . . . 18 (𝑈 No → Ord dom 𝑈)
80 ordirr 6202 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
82 disjsn 4639 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
8381, 82sylibr 235 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅)
8478, 83syl5eq 2865 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅)
85 xpdisj1 6011 . . . . . . . . . . . . . . 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 2855 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2o⟩} ∩ (dom 𝑈 × V)) = ∅)
8873, 87syl5eq 2865 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈) = ∅)
8988uneq2d 4136 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅))
90 resundir 5861 . . . . . . . . . . 11 ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2o⟩} ↾ dom 𝑈))
91 un0 4341 . . . . . . . . . . . 12 ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈)
9291eqcomi 2827 . . . . . . . . . . 11 (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅)
9389, 90, 923eqtr4g 2878 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈))
94 nofun 33053 . . . . . . . . . . . 12 (𝑈 No → Fun 𝑈)
9530, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Fun 𝑈)
96 funrel 6365 . . . . . . . . . . 11 (Fun 𝑈 → Rel 𝑈)
97 resdm 5890 . . . . . . . . . . 11 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
9895, 96, 973syl 18 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
9993, 98eqtrd 2853 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) = 𝑈)
100 sssucid 6261 . . . . . . . . . 10 dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 5876 . . . . . . . . . 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 5089 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈))
10474elexi 3511 . . . . . . . . . . . . 13 2o ∈ V
105104prid2 4691 . . . . . . . . . . . 12 2o ∈ {1o, 2o}
106105noextend 33070 . . . . . . . . . . 11 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
1078, 106syl 17 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
108107adantr 481 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No )
109 sucelon 7521 . . . . . . . . . . . 12 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
11027, 109sylib 219 . . . . . . . . . . 11 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On)
111 noreson 33064 . . . . . . . . . . 11 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
1129, 110, 111syl2anc 584 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No )
113112adantr 481 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
114 sltres 33066 . . . . . . . . 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 1363 . . . . . . . 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 5497 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
11812, 117mpan 686 . . . . . . . 8 (((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ) → ((𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
119108, 113, 118syl2anc 584 . . . . . . 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 6190 . . . . . . . . . 10 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
122121reseq2i 5843 . . . . . . . . 9 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
123 resundi 5860 . . . . . . . . 9 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
124122, 123eqtri 2841 . . . . . . . 8 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
125 dmres 5868 . . . . . . . . . . 11 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
126 simpr 485 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
127 necom 3066 . . . . . . . . . . . . . . . 16 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
128127rabbii 3471 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
129128inteqi 4871 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
1309adantr 481 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1318adantr 481 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
13221adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈𝑍)
133132necomd 3068 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
134 nosepssdm 33087 . . . . . . . . . . . . . . 15 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
135130, 131, 133, 134syl3anc 1363 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
136129, 135eqsstrid 4012 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑍)
137126, 136eqsstrrd 4003 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
138 df-ss 3949 . . . . . . . . . . . 12 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
139137, 138sylib 219 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
140125, 139syl5eq 2865 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
141140eleq2d 2895 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
142 simpr 485 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
143142fvresd 6683 . . . . . . . . . . . . . 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 6209 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
146144, 145sylan 580 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
147126eleq2d 2895 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
148147biimpar 478 . . . . . . . . . . . . . . . 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 3069 . . . . . . . . . . . . . . . 16 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
151150con2bii 359 . . . . . . . . . . . . . . 15 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
152149, 151sylibr 235 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
153143, 152eqtrd 2853 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
154153ex 413 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
155141, 154sylbid 241 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞)))
156155ralrimiv 3178 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
157 nofun 33053 . . . . . . . . . . . 12 (𝑍 No → Fun 𝑍)
158 funres 6390 . . . . . . . . . . . 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 6799 . . . . . . . . . . 11 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
162159, 160, 161syl2anc 584 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
163140, 156, 162mpbir2and 709 . . . . . . . . 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 6378 . . . . . . . . . . . 12 (Fun 𝑍𝑍 Fn dom 𝑍)
166164, 165sylib 219 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍)
167 1oex 8099 . . . . . . . . . . . . . . . . . . 19 1o ∈ V
168167prid1 4690 . . . . . . . . . . . . . . . . . 18 1o ∈ {1o, 2o}
169168nosgnn0i 33063 . . . . . . . . . . . . . . . . 17 ∅ ≠ 1o
170131, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
171 ndmfv 6693 . . . . . . . . . . . . . . . . . . 19 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
172170, 80, 1713syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅)
173172neeq1d 3072 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1o ↔ ∅ ≠ 1o))
174169, 173mpbiri 259 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠ 1o)
175174neneqd 3018 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1o)
176175intnanrd 490 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅))
177175intnanrd 490 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o))
178 simplr 765 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 <s 𝑍)
179131, 130, 55syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
180178, 179mpbid 233 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
181 fveq2 6663 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
182181adantl 482 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
183 fveq2 6663 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
184183adantl 482 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
185180, 182, 1843brtr3d 5088 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈))
186 fvex 6676 . . . . . . . . . . . . . . . . 17 (𝑈‘dom 𝑈) ∈ V
187 fvex 6676 . . . . . . . . . . . . . . . . 17 (𝑍‘dom 𝑈) ∈ V
188186, 187brtp 32882 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)))
189 3orrot 1084 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)))
190 3orrot 1084 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
191188, 189, 1903bitri 298 . . . . . . . . . . . . . . 15 ((𝑈‘dom 𝑈){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
192185, 191sylib 219 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)))
193176, 177, 192ecase23d 1464 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o))
194193simprd 496 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2o)
195 ndmfv 6693 . . . . . . . . . . . . . 14 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
196105nosgnn0i 33063 . . . . . . . . . . . . . . . 16 ∅ ≠ 2o
197 neeq1 3075 . . . . . . . . . . . . . . . 16 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2o ↔ ∅ ≠ 2o))
198196, 197mpbiri 259 . . . . . . . . . . . . . . 15 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2o)
199198neneqd 3018 . . . . . . . . . . . . . 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 6912 . . . . . . . . . . 11 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
204166, 202, 203syl2anc 584 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
205194opeq2d 4802 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 2o⟩)
206205sneqd 4569 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 2o⟩})
207204, 206eqtrd 2853 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 2o⟩})
208163, 207uneq12d 4137 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
209124, 208syl5eq 2865 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
210 sonr 5489 . . . . . . . . 9 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2o⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
21112, 210mpan 686 . . . . . . . 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 5075 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
214120, 213jaodan 951 . . . . 5 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
215214ex 413 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩})))
21629, 215sylbid 241 . . 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 683 1 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3o 1078  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557  {ctp 4561  cop 4563   cint 4867   class class class wbr 5057   Or wor 5466   × cxp 5546  dom cdm 5548  cres 5550  Rel wrel 5553  Ord word 6183  Oncon0 6184  suc csuc 6186  Fun wfun 6342   Fn wfn 6343  cfv 6348  1oc1o 8084  2oc2o 8085   No csur 33044   <s cslt 33045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-1o 8091  df-2o 8092  df-no 33047  df-slt 33048
This theorem is referenced by:  nosupbnd2  33113
  Copyright terms: Public domain W3C validator