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

Theorem nosupbnd2lem1 31986
 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 1105 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈𝐴)
2 simp3 1083 . . 3 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ∀𝑎𝐴 𝑎 <s 𝑍)
3 breq1 4688 . . . 4 (𝑎 = 𝑈 → (𝑎 <s 𝑍𝑈 <s 𝑍))
43rspcv 3336 . . 3 (𝑈𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑈 <s 𝑍))
51, 2, 4sylc 65 . 2 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍)
6 simpl21 1159 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 No )
7 simpl1l 1132 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝐴)
86, 7sseldd 3637 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 No )
9 simpl23 1161 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 No )
10 simp21 1114 . . . . . . . . . 10 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝐴 No )
1110, 1sseldd 3637 . . . . . . . . 9 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → 𝑈 No )
12 sltso 31952 . . . . . . . . . 10 <s Or No
13 sonr 5085 . . . . . . . . . 10 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
1412, 13mpan 706 . . . . . . . . 9 (𝑈 No → ¬ 𝑈 <s 𝑈)
1511, 14syl 17 . . . . . . . 8 (((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈)
16 breq2 4689 . . . . . . . . 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 2830 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈𝑍)
22 nosepssdm 31961 . . . 4 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
238, 9, 21, 22syl3anc 1366 . . 3 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈)
24 nosepon 31943 . . . . . 6 ((𝑈 No 𝑍 No 𝑈𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
258, 9, 21, 24syl3anc 1366 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
26 nodmon 31928 . . . . . 6 (𝑈 No → dom 𝑈 ∈ On)
278, 26syl 17 . . . . 5 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On)
28 onsseleq 5803 . . . . 5 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
2925, 27, 28syl2anc 694 . . . 4 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑈 ↔ ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)))
308adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 No )
319adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑍 No )
3221adantr 480 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈𝑍)
3330, 31, 32, 24syl3anc 1366 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On)
34 onelon 5786 . . . . . . . . . . . . . . . 16 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
3533, 34sylan 487 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ On)
36 simpr 476 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})
37 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑈𝑥) = (𝑈𝑞))
38 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → (𝑍𝑥) = (𝑍𝑞))
3937, 38neeq12d 2884 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑈𝑞) ≠ (𝑍𝑞)))
4039onnminsb 7046 . . . . . . . . . . . . . . 15 (𝑞 ∈ On → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ¬ (𝑈𝑞) ≠ (𝑍𝑞)))
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ¬ (𝑈𝑞) ≠ (𝑍𝑞))
42 df-ne 2824 . . . . . . . . . . . . . . 15 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑈𝑞) = (𝑍𝑞))
4342con2bii 346 . . . . . . . . . . . . . 14 ((𝑈𝑞) = (𝑍𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
4441, 43sylibr 224 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = (𝑍𝑞))
45 simplr 807 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
4627adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On)
4746adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → dom 𝑈 ∈ On)
48 ontr1 5809 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → 𝑞 ∈ dom 𝑈)
5150fvresd 6246 . . . . . . . . . . . . 13 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍𝑞))
5244, 51eqtr4d 2688 . . . . . . . . . . . 12 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) ∧ 𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) → (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
5352ralrimiva 2995 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))
54 simplr 807 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍)
55 sltval2 31934 . . . . . . . . . . . . . 14 ((𝑈 No 𝑍 No ) → (𝑈 <s 𝑍 ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
5630, 31, 55syl2anc 694 . . . . . . . . . . . . 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 476 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈)
5958fvresd 6246 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6057, 59breqtrrd 4713 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
61 raleq 3168 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)))
62 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → (𝑈𝑝) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
63 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))
6462, 63breq12d 4698 . . . . . . . . . . . . 13 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)})))
6561, 64anbi12d 747 . . . . . . . . . . . 12 (𝑝 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} → ((∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))))
6665rspcev 3340 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ On ∧ (∀𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}))) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
6733, 53, 60, 66syl12anc 1364 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝)))
68 noreson 31938 . . . . . . . . . . . 12 ((𝑍 No ∧ dom 𝑈 ∈ On) → (𝑍 ↾ dom 𝑈) ∈ No )
6931, 46, 68syl2anc 694 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No )
70 sltval 31925 . . . . . . . . . . 11 ((𝑈 No ∧ (𝑍 ↾ dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞𝑝 (𝑈𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈𝑝){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝑍 ↾ dom 𝑈)‘𝑝))))
7130, 69, 70syl2anc 694 . . . . . . . . . 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 5155 . . . . . . . . . . . . 13 ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V))
74 2on 7613 . . . . . . . . . . . . . . . 16 2𝑜 ∈ On
75 xpsng 6446 . . . . . . . . . . . . . . . 16 ((dom 𝑈 ∈ On ∧ 2𝑜 ∈ On) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7646, 74, 75sylancl 695 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2𝑜}) = {⟨dom 𝑈, 2𝑜⟩})
7776ineq1d 3846 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩ (dom 𝑈 × V)) = ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)))
78 incom 3838 . . . . . . . . . . . . . . . 16 ({dom 𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈})
79 nodmord 31931 . . . . . . . . . . . . . . . . . 18 (𝑈 No → Ord dom 𝑈)
80 ordirr 5779 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈)
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈)
82 disjsn 4278 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈)
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅)
8478, 83syl5eq 2697 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅)
85 xpdisj1 5590 . . . . . . . . . . . . . . 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 2687 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ∩ (dom 𝑈 × V)) = ∅)
8873, 87syl5eq 2697 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈) = ∅)
8988uneq2d 3800 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅))
90 resundir 5446 . . . . . . . . . . 11 ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({⟨dom 𝑈, 2𝑜⟩} ↾ dom 𝑈))
91 un0 4000 . . . . . . . . . . . 12 ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈)
9291eqcomi 2660 . . . . . . . . . . 11 (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅)
9389, 90, 923eqtr4g 2710 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈))
94 nofun 31927 . . . . . . . . . . . 12 (𝑈 No → Fun 𝑈)
9530, 94syl 17 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → Fun 𝑈)
96 funrel 5943 . . . . . . . . . . 11 (Fun 𝑈 → Rel 𝑈)
97 resdm 5476 . . . . . . . . . . 11 (Rel 𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈)
9895, 96, 973syl 18 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈)
9993, 98eqtrd 2685 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) = 𝑈)
100 sssucid 5840 . . . . . . . . . 10 dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 5462 . . . . . . . . . 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 4717 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈))
10474elexi 3244 . . . . . . . . . . . . 13 2𝑜 ∈ V
105104prid2 4330 . . . . . . . . . . . 12 2𝑜 ∈ {1𝑜, 2𝑜}
106105noextend 31944 . . . . . . . . . . 11 (𝑈 No → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
1078, 106syl 17 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
108107adantr 480 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No )
109 sucelon 7059 . . . . . . . . . . . 12 (dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On)
11027, 109sylib 208 . . . . . . . . . . 11 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On)
111 noreson 31938 . . . . . . . . . . 11 ((𝑍 No ∧ suc dom 𝑈 ∈ On) → (𝑍 ↾ suc dom 𝑈) ∈ No )
1129, 110, 111syl2anc 694 . . . . . . . . . 10 ((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No )
113112adantr 480 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No )
114 sltres 31940 . . . . . . . . 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 1366 . . . . . . . 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 31783 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
11812, 117mpan 706 . . . . . . . 8 (((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ) → ((𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩})))
119108, 113, 118syl2anc 694 . . . . . . 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 5767 . . . . . . . . . 10 suc dom 𝑈 = (dom 𝑈 ∪ {dom 𝑈})
122121reseq2i 5425 . . . . . . . . 9 (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈}))
123 resundi 5445 . . . . . . . . 9 (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
124122, 123eqtri 2673 . . . . . . . 8 (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈}))
125 dmres 5454 . . . . . . . . . . 11 dom (𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍)
126 simpr 476 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈)
127 necom 2876 . . . . . . . . . . . . . . . 16 ((𝑈𝑥) ≠ (𝑍𝑥) ↔ (𝑍𝑥) ≠ (𝑈𝑥))
128127rabbii 3216 . . . . . . . . . . . . . . 15 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
129128inteqi 4511 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)}
1309adantr 480 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 No )
1318adantr 480 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 No )
13221adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈𝑍)
133132necomd 2878 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍𝑈)
134 nosepssdm 31961 . . . . . . . . . . . . . . 15 ((𝑍 No 𝑈 No 𝑍𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
135130, 131, 133, 134syl3anc 1366 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑍𝑥) ≠ (𝑈𝑥)} ⊆ dom 𝑍)
136129, 135syl5eqss 3682 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ⊆ dom 𝑍)
137126, 136eqsstr3d 3673 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍)
138 df-ss 3621 . . . . . . . . . . . 12 (dom 𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
139137, 138sylib 208 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈)
140125, 139syl5eq 2697 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈)
141140eleq2d 2716 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈))
142 simpr 476 . . . . . . . . . . . . . . 15 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)
143142fvresd 6246 . . . . . . . . . . . . . 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 5786 . . . . . . . . . . . . . . . . 17 ((dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
146144, 145sylan 487 . . . . . . . . . . . . . . . 16 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On)
147126eleq2d 2716 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑞 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} ↔ 𝑞 ∈ dom 𝑈))
148147biimpar 501 . . . . . . . . . . . . . . . 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 2879 . . . . . . . . . . . . . . . 16 ((𝑈𝑞) ≠ (𝑍𝑞) ↔ ¬ (𝑍𝑞) = (𝑈𝑞))
151150con2bii 346 . . . . . . . . . . . . . . 15 ((𝑍𝑞) = (𝑈𝑞) ↔ ¬ (𝑈𝑞) ≠ (𝑍𝑞))
152149, 151sylibr 224 . . . . . . . . . . . . . 14 ((((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍𝑞) = (𝑈𝑞))
153143, 152eqtrd 2685 . . . . . . . . . . . . 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 2994 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))
157 nofun 31927 . . . . . . . . . . . 12 (𝑍 No → Fun 𝑍)
158 funres 5967 . . . . . . . . . . . 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 6356 . . . . . . . . . . 11 ((Fun (𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
162159, 160, 161syl2anc 694 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈𝑞))))
163140, 156, 162mpbir2and 977 . . . . . . . . 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 5956 . . . . . . . . . . . 12 (Fun 𝑍𝑍 Fn dom 𝑍)
166164, 165sylib 208 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍)
167 1on 7612 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ On
168167elexi 3244 . . . . . . . . . . . . . . . . . . 19 1𝑜 ∈ V
169168prid1 4329 . . . . . . . . . . . . . . . . . 18 1𝑜 ∈ {1𝑜, 2𝑜}
170169nosgnn0i 31937 . . . . . . . . . . . . . . . . 17 ∅ ≠ 1𝑜
171131, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → Ord dom 𝑈)
172 ndmfv 6256 . . . . . . . . . . . . . . . . . . 19 (¬ dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅)
173171, 80, 1723syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅)
174173neeq1d 2882 . . . . . . . . . . . . . . . . 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 2828 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1𝑜)
177176intnanrd 983 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅))
178176intnanrd 983 . . . . . . . . . . . . . 14 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜))
179 simplr 807 . . . . . . . . . . . . . . . . 17 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → 𝑈 <s 𝑍)
180131, 130, 55syl2anc 694 . . . . . . . . . . . . . . . . 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 6229 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
183182adantl 481 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑈‘dom 𝑈))
184 fveq2 6229 . . . . . . . . . . . . . . . . 17 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈 → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
185184adantl 481 . . . . . . . . . . . . . . . 16 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)}) = (𝑍‘dom 𝑈))
186181, 183, 1853brtr3d 4716 . . . . . . . . . . . . . . 15 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈))
187 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝑈‘dom 𝑈) ∈ V
188 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝑍‘dom 𝑈) ∈ V
189187, 188brtp 31765 . . . . . . . . . . . . . . . 16 ((𝑈‘dom 𝑈){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)))
190 3orrot 1061 . . . . . . . . . . . . . . . 16 ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)))
191 3orrot 1061 . . . . . . . . . . . . . . . 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 1476 . . . . . . . . . . . . 13 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜))
195194simprd 478 . . . . . . . . . . . 12 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2𝑜)
196 ndmfv 6256 . . . . . . . . . . . . . 14 (¬ dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅)
197105nosgnn0i 31937 . . . . . . . . . . . . . . . 16 ∅ ≠ 2𝑜
198 neeq1 2885 . . . . . . . . . . . . . . . 16 ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2𝑜 ↔ ∅ ≠ 2𝑜))
199197, 198mpbiri 248 . . . . . . . . . . . . . . 15 ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2𝑜)
200199neneqd 2828 . . . . . . . . . . . . . 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 6465 . . . . . . . . . . 11 ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
205166, 203, 204syl2anc 694 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩})
206195opeq2d 4440 . . . . . . . . . . 11 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ⟨dom 𝑈, (𝑍‘dom 𝑈)⟩ = ⟨dom 𝑈, 2𝑜⟩)
207206sneqd 4222 . . . . . . . . . 10 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → {⟨dom 𝑈, (𝑍‘dom 𝑈)⟩} = {⟨dom 𝑈, 2𝑜⟩})
208205, 207eqtrd 2685 . . . . . . . . 9 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {⟨dom 𝑈, 2𝑜⟩})
209163, 208uneq12d 3801 . . . . . . . 8 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
210124, 209syl5eq 2697 . . . . . . 7 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
211 sonr 5085 . . . . . . . . 9 (( <s Or No ∧ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) ∈ No ) → ¬ (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
21212, 211mpan 706 . . . . . . . 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 4703 . . . . . 6 (((((𝑈𝐴 ∧ ∀𝑦𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑍𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2𝑜⟩}))
215120, 214jaodan 843 . . . . 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 703 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 1053   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  {ctp 4214  ⟨cop 4216  ∩ cint 4507   class class class wbr 4685   Or wor 5063   × cxp 5141  dom cdm 5143   ↾ cres 5145  Rel wrel 5148  Ord word 5760  Oncon0 5761  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  ‘cfv 5926  1𝑜c1o 7598  2𝑜c2o 7599   No csur 31918
 Copyright terms: Public domain W3C validator