Metamath Proof Explorer

Theorem nosupbnd2lem1

Description: Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosupbnd2lem1 ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → 𝑈 ∈ 𝐴 )
2 simp3 ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 )
3 breq1 ⊢ ( 𝑎 = 𝑈 → ( 𝑎 <s 𝑍 ↔ 𝑈 <s 𝑍 ) )
4 3 rspcv ⊢ ( 𝑈 ∈ 𝐴 → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 → 𝑈 <s 𝑍 ) )
5 1 2 4 sylc ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → 𝑈 <s 𝑍 )
6 simpl21 ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → 𝐴 ⊆ No )
7 simpl1l ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → 𝑈 ∈ 𝐴 )
8 6 7 sseldd ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → 𝑈 ∈ No )
9 simpl23 ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → 𝑍 ∈ No )
10 simp21 ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → 𝐴 ⊆ No )
11 10 1 sseldd ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → 𝑈 ∈ No )
12 ltsso ⊢ <s Or No
13 sonr ⊢ ( ( <s Or No ∧ 𝑈 ∈ No ) → ¬ 𝑈 <s 𝑈 )
14 12 13 mpan ⊢ ( 𝑈 ∈ No → ¬ 𝑈 <s 𝑈 )
15 11 14 syl ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ¬ 𝑈 <s 𝑈 )
16 breq2 ⊢ ( 𝑈 = 𝑍 → ( 𝑈 <s 𝑈 ↔ 𝑈 <s 𝑍 ) )
17 16 notbid ⊢ ( 𝑈 = 𝑍 → ( ¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍 ) )
18 15 17 syl5ibcom ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ( 𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍 ) )
19 18 con2d ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ( 𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍 ) )
20 19 imp ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ¬ 𝑈 = 𝑍 )
21 20 neqned ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → 𝑈 ≠ 𝑍 )
22 nosepssdm ⊢ ( ( 𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 )
23 8 9 21 22 syl3anc ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 )
24 nosepon ⊢ ( ( 𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On )
25 8 9 21 24 syl3anc ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On )
26 nodmon ⊢ ( 𝑈 ∈ No → dom 𝑈 ∈ On )
27 8 26 syl ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → dom 𝑈 ∈ On )
28 onsseleq ⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On ∧ dom 𝑈 ∈ On ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 ↔ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) )
29 25 27 28 syl2anc ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 ↔ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) )
30 8 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑈 ∈ No )
31 9 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑍 ∈ No )
32 21 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑈 ≠ 𝑍 )
33 30 31 32 24 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On )
34 onelon ⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → 𝑞 ∈ On )
35 33 34 sylan ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → 𝑞 ∈ On )
36 simpr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } )
37 fveq2 ⊢ ( 𝑥 = 𝑞 → ( 𝑈 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑞 ) )
38 fveq2 ⊢ ( 𝑥 = 𝑞 → ( 𝑍 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑞 ) )
39 37 38 neeq12d ⊢ ( 𝑥 = 𝑞 → ( ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) ↔ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ) )
40 39 onnminsb ⊢ ( 𝑞 ∈ On → ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ) )
41 35 36 40 sylc ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
42 df-ne ⊢ ( ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ↔ ¬ ( 𝑈 ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
43 42 con2bii ⊢ ( ( 𝑈 ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) ↔ ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
44 41 43 sylibr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ( 𝑈 ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
45 simplr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 )
46 27 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → dom 𝑈 ∈ On )
47 46 adantr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → dom 𝑈 ∈ On )
48 ontr1 ⊢ ( dom 𝑈 ∈ On → ( ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑞 ∈ dom 𝑈 ) )
49 47 48 syl ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ( ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑞 ∈ dom 𝑈 ) )
50 36 45 49 mp2and ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → 𝑞 ∈ dom 𝑈 )
51 50 fvresd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
52 44 51 eqtr4d ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) ∧ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) → ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) )
53 52 ralrimiva ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ∀ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) )
54 simplr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑈 <s 𝑍 )
55 ltsval2 ⊢ ( ( 𝑈 ∈ No ∧ 𝑍 ∈ No ) → ( 𝑈 <s 𝑍 ↔ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) )
56 30 31 55 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 <s 𝑍 ↔ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) )
57 54 56 mpbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
58 simpr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 )
59 58 fvresd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
60 57 59 breqtrrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
61 raleq ⊢ ( 𝑝 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ↔ ∀ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ) )
62 fveq2 ⊢ ( 𝑝 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ( 𝑈 ‘ 𝑝 ) = ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
63 fveq2 ⊢ ( 𝑝 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
64 62 63 breq12d ⊢ ( 𝑝 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ( ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ↔ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) )
65 61 64 anbi12d ⊢ ( 𝑝 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } → ( ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ) ↔ ( ∀ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) ) )
66 65 rspcev ⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On ∧ ( ∀ 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) ) → ∃ 𝑝 ∈ On ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ) )
67 33 53 60 66 syl12anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ∃ 𝑝 ∈ On ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ) )
68 noreson ⊢ ( ( 𝑍 ∈ No ∧ dom 𝑈 ∈ On ) → ( 𝑍 ↾ dom 𝑈 ) ∈ No )
69 31 46 68 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑍 ↾ dom 𝑈 ) ∈ No )
70 ltsval ⊢ ( ( 𝑈 ∈ No ∧ ( 𝑍 ↾ dom 𝑈 ) ∈ No ) → ( 𝑈 <s ( 𝑍 ↾ dom 𝑈 ) ↔ ∃ 𝑝 ∈ On ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ) ) )
71 30 69 70 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 <s ( 𝑍 ↾ dom 𝑈 ) ↔ ∃ 𝑝 ∈ On ( ∀ 𝑞 ∈ 𝑝 ( 𝑈 ‘ 𝑞 ) = ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) ∧ ( 𝑈 ‘ 𝑝 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑝 ) ) ) )
72 67 71 mpbird ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → 𝑈 <s ( 𝑍 ↾ dom 𝑈 ) )
73 df-res ⊢ ( { ⟨ dom 𝑈 , 2o ⟩ } ↾ dom 𝑈 ) = ( { ⟨ dom 𝑈 , 2o ⟩ } ∩ ( dom 𝑈 × V ) )
74 2on ⊢ 2o ∈ On
75 xpsng ⊢ ( ( dom 𝑈 ∈ On ∧ 2o ∈ On ) → ( { dom 𝑈 } × { 2o } ) = { ⟨ dom 𝑈 , 2o ⟩ } )
76 46 74 75 sylancl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( { dom 𝑈 } × { 2o } ) = { ⟨ dom 𝑈 , 2o ⟩ } )
77 76 ineq1d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( { dom 𝑈 } × { 2o } ) ∩ ( dom 𝑈 × V ) ) = ( { ⟨ dom 𝑈 , 2o ⟩ } ∩ ( dom 𝑈 × V ) ) )
78 incom ⊢ ( { dom 𝑈 } ∩ dom 𝑈 ) = ( dom 𝑈 ∩ { dom 𝑈 } )
79 nodmord ⊢ ( 𝑈 ∈ No → Ord dom 𝑈 )
80 ordirr ⊢ ( Ord dom 𝑈 → ¬ dom 𝑈 ∈ dom 𝑈 )
81 30 79 80 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ¬ dom 𝑈 ∈ dom 𝑈 )
82 disjsn ⊢ ( ( dom 𝑈 ∩ { dom 𝑈 } ) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈 )
83 81 82 sylibr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( dom 𝑈 ∩ { dom 𝑈 } ) = ∅ )
84 78 83 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( { dom 𝑈 } ∩ dom 𝑈 ) = ∅ )
85 xpdisj1 ⊢ ( ( { dom 𝑈 } ∩ dom 𝑈 ) = ∅ → ( ( { dom 𝑈 } × { 2o } ) ∩ ( dom 𝑈 × V ) ) = ∅ )
86 84 85 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( { dom 𝑈 } × { 2o } ) ∩ ( dom 𝑈 × V ) ) = ∅ )
87 77 86 eqtr3d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( { ⟨ dom 𝑈 , 2o ⟩ } ∩ ( dom 𝑈 × V ) ) = ∅ )
88 73 87 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( { ⟨ dom 𝑈 , 2o ⟩ } ↾ dom 𝑈 ) = ∅ )
89 88 uneq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ↾ dom 𝑈 ) ∪ ( { ⟨ dom 𝑈 , 2o ⟩ } ↾ dom 𝑈 ) ) = ( ( 𝑈 ↾ dom 𝑈 ) ∪ ∅ ) )
90 resundir ⊢ ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) = ( ( 𝑈 ↾ dom 𝑈 ) ∪ ( { ⟨ dom 𝑈 , 2o ⟩ } ↾ dom 𝑈 ) )
91 un0 ⊢ ( ( 𝑈 ↾ dom 𝑈 ) ∪ ∅ ) = ( 𝑈 ↾ dom 𝑈 )
92 91 eqcomi ⊢ ( 𝑈 ↾ dom 𝑈 ) = ( ( 𝑈 ↾ dom 𝑈 ) ∪ ∅ )
93 89 90 92 3eqtr4g ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) = ( 𝑈 ↾ dom 𝑈 ) )
94 nofun ⊢ ( 𝑈 ∈ No → Fun 𝑈 )
95 funrel ⊢ ( Fun 𝑈 → Rel 𝑈 )
96 resdm ⊢ ( Rel 𝑈 → ( 𝑈 ↾ dom 𝑈 ) = 𝑈 )
97 30 94 95 96 4syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ↾ dom 𝑈 ) = 𝑈 )
98 93 97 eqtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) = 𝑈 )
99 sssucid ⊢ dom 𝑈 ⊆ suc dom 𝑈
100 resabs1 ⊢ ( dom 𝑈 ⊆ suc dom 𝑈 → ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) = ( 𝑍 ↾ dom 𝑈 ) )
101 99 100 mp1i ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) = ( 𝑍 ↾ dom 𝑈 ) )
102 72 98 101 3brtr4d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) )
103 74 elexi ⊢ 2o ∈ V
104 103 prid2 ⊢ 2o ∈ { 1o , 2o }
105 104 noextend ⊢ ( 𝑈 ∈ No → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
106 8 105 syl ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
107 106 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
108 onsucb ⊢ ( dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On )
109 27 108 sylib ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → suc dom 𝑈 ∈ On )
110 noreson ⊢ ( ( 𝑍 ∈ No ∧ suc dom 𝑈 ∈ On ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
111 9 109 110 syl2anc ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
112 111 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
113 ltsres ⊢ ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ∧ dom 𝑈 ∈ On ) → ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) ) )
114 107 112 46 113 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) ) )
115 102 114 mpd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )
116 soasym ⊢ ( ( <s Or No ∧ ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ) ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
117 12 116 mpan ⊢ ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
118 107 112 117 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
119 115 118 mpd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
120 df-suc ⊢ suc dom 𝑈 = ( dom 𝑈 ∪ { dom 𝑈 } )
121 120 reseq2i ⊢ ( 𝑍 ↾ suc dom 𝑈 ) = ( 𝑍 ↾ ( dom 𝑈 ∪ { dom 𝑈 } ) )
122 resundi ⊢ ( 𝑍 ↾ ( dom 𝑈 ∪ { dom 𝑈 } ) ) = ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) )
123 121 122 eqtri ⊢ ( 𝑍 ↾ suc dom 𝑈 ) = ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) )
124 dmres ⊢ dom ( 𝑍 ↾ dom 𝑈 ) = ( dom 𝑈 ∩ dom 𝑍 )
125 simpr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 )
126 necom ⊢ ( ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) ↔ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) )
127 126 rabbii ⊢ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) }
128 127 inteqi ⊢ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) }
129 9 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ∈ No )
130 8 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 ∈ No )
131 21 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 ≠ 𝑍 )
132 131 necomd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ≠ 𝑈 )
133 nosepssdm ⊢ ( ( 𝑍 ∈ No ∧ 𝑈 ∈ No ∧ 𝑍 ≠ 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
134 129 130 132 133 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
135 128 134 eqsstrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑍 )
136 125 135 eqsstrrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ⊆ dom 𝑍 )
137 dfss2 ⊢ ( dom 𝑈 ⊆ dom 𝑍 ↔ ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
138 136 137 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
139 124 138 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 )
140 139 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ↔ 𝑞 ∈ dom 𝑈 ) )
141 simpr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ dom 𝑈 )
142 141 fvresd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
143 130 26 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ On )
144 onelon ⊢ ( ( dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
145 143 144 sylan ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
146 125 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ↔ 𝑞 ∈ dom 𝑈 ) )
147 146 biimpar ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } )
148 145 147 40 sylc ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
149 nesym ⊢ ( ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ↔ ¬ ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
150 149 con2bii ⊢ ( ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ↔ ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
151 148 150 sylibr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
152 142 151 eqtrd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
153 152 ex ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom 𝑈 → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
154 140 153 sylbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
155 154 ralrimiv ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
156 nofun ⊢ ( 𝑍 ∈ No → Fun 𝑍 )
157 funres ⊢ ( Fun 𝑍 → Fun ( 𝑍 ↾ dom 𝑈 ) )
158 129 156 157 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun ( 𝑍 ↾ dom 𝑈 ) )
159 130 94 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑈 )
160 eqfunfv ⊢ ( ( Fun ( 𝑍 ↾ dom 𝑈 ) ∧ Fun 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
161 158 159 160 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
162 139 155 161 mpbir2and ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ dom 𝑈 ) = 𝑈 )
163 129 156 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑍 )
164 funfn ⊢ ( Fun 𝑍 ↔ 𝑍 Fn dom 𝑍 )
165 163 164 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 Fn dom 𝑍 )
166 1oex ⊢ 1o ∈ V
167 166 prid1 ⊢ 1o ∈ { 1o , 2o }
168 167 nosgnn0i ⊢ ∅ ≠ 1o
169 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑈 ) = ∅ )
170 130 79 80 169 4syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) = ∅ )
171 170 neeq1d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑈 ‘ dom 𝑈 ) ≠ 1o ↔ ∅ ≠ 1o ) )
172 168 171 mpbiri ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) ≠ 1o )
173 172 neneqd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ‘ dom 𝑈 ) = 1o )
174 173 intnanrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) )
175 173 intnanrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) )
176 simplr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 <s 𝑍 )
177 130 129 55 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 <s 𝑍 ↔ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) )
178 176 177 mpbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
179 fveq2 ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑈 ‘ dom 𝑈 ) )
180 179 adantl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑈 ‘ dom 𝑈 ) )
181 fveq2 ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑍 ‘ dom 𝑈 ) )
182 181 adantl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑍 ‘ dom 𝑈 ) )
183 178 180 182 3brtr3d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) )
184 fvex ⊢ ( 𝑈 ‘ dom 𝑈 ) ∈ V
185 fvex ⊢ ( 𝑍 ‘ dom 𝑈 ) ∈ V
186 184 185 brtp ⊢ ( ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
187 3orrot ⊢ ( ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ) )
188 3orrot ⊢ ( ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
189 186 187 188 3bitri ⊢ ( ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
190 183 189 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
191 174 175 190 ecase23d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) )
192 191 simprd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ dom 𝑈 ) = 2o )
193 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ( 𝑍 ‘ dom 𝑈 ) = ∅ )
194 104 nosgnn0i ⊢ ∅ ≠ 2o
195 neeq1 ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( ( 𝑍 ‘ dom 𝑈 ) ≠ 2o ↔ ∅ ≠ 2o ) )
196 194 195 mpbiri ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( 𝑍 ‘ dom 𝑈 ) ≠ 2o )
197 196 neneqd ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ¬ ( 𝑍 ‘ dom 𝑈 ) = 2o )
198 193 197 syl ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ¬ ( 𝑍 ‘ dom 𝑈 ) = 2o )
199 198 con4i ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = 2o → dom 𝑈 ∈ dom 𝑍 )
200 192 199 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ dom 𝑍 )
201 fnressn ⊢ ( ( 𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
202 165 200 201 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
203 192 opeq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ = ⟨ dom 𝑈 , 2o ⟩ )
204 203 sneqd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } = { ⟨ dom 𝑈 , 2o ⟩ } )
205 202 204 eqtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , 2o ⟩ } )
206 162 205 uneq12d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
207 123 206 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ suc dom 𝑈 ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
208 sonr ⊢ ( ( <s Or No ∧ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
209 12 208 mpan ⊢ ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
210 130 105 209 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
211 207 210 eqnbrtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
212 119 211 jaodan ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
213 212 ex ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
214 29 213 sylbid ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
215 23 214 mpd ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
216 5 215 mpdan ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )