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 sltso ⊢ <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 sltval2 ⊢ ( ( 𝑈 ∈ 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 sltval ⊢ ( ( 𝑈 ∈ 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 30 94 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → Fun 𝑈 )
96 funrel ⊢ ( Fun 𝑈 → Rel 𝑈 )
97 resdm ⊢ ( Rel 𝑈 → ( 𝑈 ↾ dom 𝑈 ) = 𝑈 )
98 95 96 97 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ↾ dom 𝑈 ) = 𝑈 )
99 93 98 eqtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) = 𝑈 )
100 sssucid ⊢ dom 𝑈 ⊆ suc dom 𝑈
101 resabs1 ⊢ ( dom 𝑈 ⊆ suc dom 𝑈 → ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) = ( 𝑍 ↾ dom 𝑈 ) )
102 100 101 mp1i ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) = ( 𝑍 ↾ dom 𝑈 ) )
103 72 99 102 3brtr4d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) )
104 74 elexi ⊢ 2o ∈ V
105 104 prid2 ⊢ 2o ∈ { 1o , 2o }
106 105 noextend ⊢ ( 𝑈 ∈ No → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
107 8 106 syl ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
108 107 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No )
109 sucelon ⊢ ( dom 𝑈 ∈ On ↔ suc dom 𝑈 ∈ On )
110 27 109 sylib ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → suc dom 𝑈 ∈ On )
111 noreson ⊢ ( ( 𝑍 ∈ No ∧ suc dom 𝑈 ∈ On ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
112 9 110 111 syl2anc ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
113 112 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑍 ↾ suc dom 𝑈 ) ∈ No )
114 sltres ⊢ ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ∧ dom 𝑈 ∈ On ) → ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) ) )
115 108 113 46 114 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ↾ dom 𝑈 ) <s ( ( 𝑍 ↾ suc dom 𝑈 ) ↾ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) ) )
116 103 115 mpd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )
117 soasym ⊢ ( ( <s Or No ∧ ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ) ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
118 12 117 mpan ⊢ ( ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ∧ ( 𝑍 ↾ suc dom 𝑈 ) ∈ No ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
119 108 113 118 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
120 116 119 mpd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
121 df-suc ⊢ suc dom 𝑈 = ( dom 𝑈 ∪ { dom 𝑈 } )
122 121 reseq2i ⊢ ( 𝑍 ↾ suc dom 𝑈 ) = ( 𝑍 ↾ ( dom 𝑈 ∪ { dom 𝑈 } ) )
123 resundi ⊢ ( 𝑍 ↾ ( dom 𝑈 ∪ { dom 𝑈 } ) ) = ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) )
124 122 123 eqtri ⊢ ( 𝑍 ↾ suc dom 𝑈 ) = ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) )
125 dmres ⊢ dom ( 𝑍 ↾ dom 𝑈 ) = ( dom 𝑈 ∩ dom 𝑍 )
126 simpr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 )
127 necom ⊢ ( ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) ↔ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) )
128 127 rabbii ⊢ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) }
129 128 inteqi ⊢ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) }
130 9 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ∈ No )
131 8 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 ∈ No )
132 21 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 ≠ 𝑍 )
133 132 necomd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ≠ 𝑈 )
134 nosepssdm ⊢ ( ( 𝑍 ∈ No ∧ 𝑈 ∈ No ∧ 𝑍 ≠ 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
135 130 131 133 134 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
136 129 135 eqsstrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑍 )
137 126 136 eqsstrrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ⊆ dom 𝑍 )
138 df-ss ⊢ ( dom 𝑈 ⊆ dom 𝑍 ↔ ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
139 137 138 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
140 125 139 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 )
141 140 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ↔ 𝑞 ∈ dom 𝑈 ) )
142 simpr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ dom 𝑈 )
143 142 fvresd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
144 131 26 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ On )
145 onelon ⊢ ( ( dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
146 144 145 sylan ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
147 126 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ↔ 𝑞 ∈ dom 𝑈 ) )
148 147 biimpar ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } )
149 146 148 40 sylc ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
150 nesym ⊢ ( ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ↔ ¬ ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
151 150 con2bii ⊢ ( ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ↔ ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
152 149 151 sylibr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
153 143 152 eqtrd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
154 153 ex ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom 𝑈 → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
155 141 154 sylbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
156 155 ralrimiv ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
157 nofun ⊢ ( 𝑍 ∈ No → Fun 𝑍 )
158 funres ⊢ ( Fun 𝑍 → Fun ( 𝑍 ↾ dom 𝑈 ) )
159 130 157 158 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun ( 𝑍 ↾ dom 𝑈 ) )
160 131 94 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑈 )
161 eqfunfv ⊢ ( ( Fun ( 𝑍 ↾ dom 𝑈 ) ∧ Fun 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
162 159 160 161 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
163 140 156 162 mpbir2and ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ dom 𝑈 ) = 𝑈 )
164 130 157 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑍 )
165 funfn ⊢ ( Fun 𝑍 ↔ 𝑍 Fn dom 𝑍 )
166 164 165 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 Fn dom 𝑍 )
167 1oex ⊢ 1o ∈ V
168 167 prid1 ⊢ 1o ∈ { 1o , 2o }
169 168 nosgnn0i ⊢ ∅ ≠ 1o
170 131 79 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Ord dom 𝑈 )
171 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑈 ) = ∅ )
172 170 80 171 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) = ∅ )
173 172 neeq1d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑈 ‘ dom 𝑈 ) ≠ 1o ↔ ∅ ≠ 1o ) )
174 169 173 mpbiri ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) ≠ 1o )
175 174 neneqd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ‘ dom 𝑈 ) = 1o )
176 175 intnanrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) )
177 175 intnanrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) )
178 simplr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 <s 𝑍 )
179 131 130 55 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 <s 𝑍 ↔ ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) ) )
180 178 179 mpbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) )
181 fveq2 ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑈 ‘ dom 𝑈 ) )
182 181 adantl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑈 ‘ dom 𝑈 ) )
183 fveq2 ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑍 ‘ dom 𝑈 ) )
184 183 adantl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ) = ( 𝑍 ‘ dom 𝑈 ) )
185 180 182 184 3brtr3d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) )
186 fvex ⊢ ( 𝑈 ‘ dom 𝑈 ) ∈ V
187 fvex ⊢ ( 𝑍 ‘ dom 𝑈 ) ∈ V
188 186 187 brtp ⊢ ( ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
189 3orrot ⊢ ( ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ) )
190 3orrot ⊢ ( ( ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
191 188 189 190 3bitri ⊢ ( ( 𝑈 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑍 ‘ dom 𝑈 ) ↔ ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
192 185 191 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑈 ‘ dom 𝑈 ) = 1o ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) ) )
193 176 177 192 ecase23d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑍 ‘ dom 𝑈 ) = 2o ) )
194 193 simprd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ dom 𝑈 ) = 2o )
195 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ( 𝑍 ‘ dom 𝑈 ) = ∅ )
196 105 nosgnn0i ⊢ ∅ ≠ 2o
197 neeq1 ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( ( 𝑍 ‘ dom 𝑈 ) ≠ 2o ↔ ∅ ≠ 2o ) )
198 196 197 mpbiri ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( 𝑍 ‘ dom 𝑈 ) ≠ 2o )
199 198 neneqd ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ¬ ( 𝑍 ‘ dom 𝑈 ) = 2o )
200 195 199 syl ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ¬ ( 𝑍 ‘ dom 𝑈 ) = 2o )
201 200 con4i ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = 2o → dom 𝑈 ∈ dom 𝑍 )
202 194 201 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ dom 𝑍 )
203 fnressn ⊢ ( ( 𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
204 166 202 203 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
205 194 opeq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ = ⟨ dom 𝑈 , 2o ⟩ )
206 205 sneqd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } = { ⟨ dom 𝑈 , 2o ⟩ } )
207 204 206 eqtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , 2o ⟩ } )
208 163 207 uneq12d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
209 124 208 eqtrid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ suc dom 𝑈 ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
210 sonr ⊢ ( ( <s Or No ∧ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
211 12 210 mpan ⊢ ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ∈ No → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
212 131 106 211 3syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
213 209 212 eqnbrtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
214 120 213 jaodan ⊢ ( ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) ∧ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
215 214 ex ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
216 29 215 sylbid ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) ) )
217 23 216 mpd ⊢ ( ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) ∧ 𝑈 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )
218 5 217 mpdan ⊢ ( ( ( 𝑈 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦 ) ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑍 ) → ¬ ( 𝑍 ↾ suc dom 𝑈 ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 2o ⟩ } ) )