Metamath Proof Explorer

Theorem noinfbnd2lem1

Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion noinfbnd2lem1 ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )

Proof

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