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 sltval2 ⊢ ( ( 𝑍 ∈ 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 sltval ⊢ ( ( ( 𝑍 ↾ 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 syl5eq ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <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 sucelon ⊢ ( 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 sltres ⊢ ( ( ( 𝑍 ↾ 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 sltso ⊢ <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 biimpi ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } = dom 𝑈 )
110 109 adantl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } = dom 𝑈 )
111 35 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ∈ No )
112 7 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑈 ∈ No )
113 simp23 ⊢ ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → 𝑍 ∈ No )
114 sonr ⊢ ( ( <s Or No ∧ 𝑍 ∈ No ) → ¬ 𝑍 <s 𝑍 )
115 95 113 114 sylancr ⊢ ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ 𝑍 <s 𝑍 )
116 breq2 ⊢ ( 𝑈 = 𝑍 → ( 𝑍 <s 𝑈 ↔ 𝑍 <s 𝑍 ) )
117 116 notbid ⊢ ( 𝑈 = 𝑍 → ( ¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍 ) )
118 115 117 syl5ibrcom ⊢ ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ( 𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈 ) )
119 118 necon2ad ⊢ ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ( 𝑍 <s 𝑈 → 𝑈 ≠ 𝑍 ) )
120 119 imp ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → 𝑈 ≠ 𝑍 )
121 120 necomd ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → 𝑍 ≠ 𝑈 )
122 121 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → 𝑍 ≠ 𝑈 )
123 nosepssdm ⊢ ( ( 𝑍 ∈ No ∧ 𝑈 ∈ No ∧ 𝑍 ≠ 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
124 111 112 122 123 syl3anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ⊆ dom 𝑍 )
125 110 124 eqsstrrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ⊆ dom 𝑍 )
126 df-ss ⊢ ( dom 𝑈 ⊆ dom 𝑍 ↔ ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
127 125 126 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( dom 𝑈 ∩ dom 𝑍 ) = dom 𝑈 )
128 107 127 syl5eq ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 )
129 128 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ↔ 𝑞 ∈ dom 𝑈 ) )
130 simpr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ dom 𝑈 )
131 130 fvresd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑍 ‘ 𝑞 ) )
132 112 8 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ On )
133 onelon ⊢ ( ( dom 𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
134 132 133 sylan ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ On )
135 simpr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 )
136 135 eleq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ↔ 𝑞 ∈ dom 𝑈 ) )
137 136 biimpar ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → 𝑞 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } )
138 134 137 25 sylc ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
139 nesym ⊢ ( ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) ↔ ¬ ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
140 139 con2bii ⊢ ( ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ↔ ¬ ( 𝑈 ‘ 𝑞 ) ≠ ( 𝑍 ‘ 𝑞 ) )
141 138 140 sylibr ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( 𝑍 ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
142 131 141 eqtrd ⊢ ( ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ∧ 𝑞 ∈ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
143 142 ex ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom 𝑈 → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
144 129 143 sylbid ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) )
145 144 ralrimiv ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) )
146 nofun ⊢ ( 𝑍 ∈ No → Fun 𝑍 )
147 111 146 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑍 )
148 147 funresd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun ( 𝑍 ↾ dom 𝑈 ) )
149 64 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Fun 𝑈 )
150 eqfunfv ⊢ ( ( Fun ( 𝑍 ↾ dom 𝑈 ) ∧ Fun 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
151 148 149 150 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) = 𝑈 ↔ ( dom ( 𝑍 ↾ dom 𝑈 ) = dom 𝑈 ∧ ∀ 𝑞 ∈ dom ( 𝑍 ↾ dom 𝑈 ) ( ( 𝑍 ↾ dom 𝑈 ) ‘ 𝑞 ) = ( 𝑈 ‘ 𝑞 ) ) ) )
152 128 145 151 mpbir2and ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ dom 𝑈 ) = 𝑈 )
153 35 146 syl ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → Fun 𝑍 )
154 153 funfnd ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → 𝑍 Fn dom 𝑍 )
155 112 70 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → Ord dom 𝑈 )
156 155 73 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ dom 𝑈 ∈ dom 𝑈 )
157 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑈 ) = ∅ )
158 2on0 ⊢ 2o ≠ ∅
159 158 necomi ⊢ ∅ ≠ 2o
160 neeq1 ⊢ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ → ( ( 𝑈 ‘ dom 𝑈 ) ≠ 2o ↔ ∅ ≠ 2o ) )
161 159 160 mpbiri ⊢ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ → ( 𝑈 ‘ dom 𝑈 ) ≠ 2o )
162 161 neneqd ⊢ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ → ¬ ( 𝑈 ‘ dom 𝑈 ) = 2o )
163 157 162 syl ⊢ ( ¬ dom 𝑈 ∈ dom 𝑈 → ¬ ( 𝑈 ‘ dom 𝑈 ) = 2o )
164 156 163 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ‘ dom 𝑈 ) = 2o )
165 164 intnand ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) )
166 simpr ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → 𝑍 <s 𝑈 )
167 35 7 37 syl2anc ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ( 𝑍 <s 𝑈 ↔ ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) ) )
168 166 167 mpbid ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) )
169 168 adantr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) )
170 110 fveq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) = ( 𝑍 ‘ dom 𝑈 ) )
171 110 fveq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑍 ‘ 𝑥 ) ≠ ( 𝑈 ‘ 𝑥 ) } ) = ( 𝑈 ‘ dom 𝑈 ) )
172 169 170 171 3brtr3d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑈 ‘ dom 𝑈 ) )
173 fvex ⊢ ( 𝑍 ‘ dom 𝑈 ) ∈ V
174 fvex ⊢ ( 𝑈 ‘ dom 𝑈 ) ∈ V
175 173 174 brtp ⊢ ( ( 𝑍 ‘ dom 𝑈 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑈 ‘ dom 𝑈 ) ↔ ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) )
176 172 175 sylib ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) )
177 3orel3 ⊢ ( ¬ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) → ( ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) → ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) ) )
178 165 176 177 sylc ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) )
179 andi ⊢ ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∨ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) ↔ ( ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = ∅ ) ∨ ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) )
180 178 179 sylibr ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ‘ dom 𝑈 ) = 1o ∧ ( ( 𝑈 ‘ dom 𝑈 ) = ∅ ∨ ( 𝑈 ‘ dom 𝑈 ) = 2o ) ) )
181 180 simpld ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ‘ dom 𝑈 ) = 1o )
182 ndmfv ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ( 𝑍 ‘ dom 𝑈 ) = ∅ )
183 1n0 ⊢ 1o ≠ ∅
184 183 necomi ⊢ ∅ ≠ 1o
185 neeq1 ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( ( 𝑍 ‘ dom 𝑈 ) ≠ 1o ↔ ∅ ≠ 1o ) )
186 184 185 mpbiri ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ( 𝑍 ‘ dom 𝑈 ) ≠ 1o )
187 186 neneqd ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = ∅ → ¬ ( 𝑍 ‘ dom 𝑈 ) = 1o )
188 182 187 syl ⊢ ( ¬ dom 𝑈 ∈ dom 𝑍 → ¬ ( 𝑍 ‘ dom 𝑈 ) = 1o )
189 188 con4i ⊢ ( ( 𝑍 ‘ dom 𝑈 ) = 1o → dom 𝑈 ∈ dom 𝑍 )
190 181 189 syl ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → dom 𝑈 ∈ dom 𝑍 )
191 fnressn ⊢ ( ( 𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
192 154 190 191 syl2an2r ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } )
193 181 opeq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ = ⟨ dom 𝑈 , 1o ⟩ )
194 193 sneqd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → { ⟨ dom 𝑈 , ( 𝑍 ‘ dom 𝑈 ) ⟩ } = { ⟨ dom 𝑈 , 1o ⟩ } )
195 192 194 eqtrd ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ { dom 𝑈 } ) = { ⟨ dom 𝑈 , 1o ⟩ } )
196 152 195 uneq12d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑍 ↾ dom 𝑈 ) ∪ ( 𝑍 ↾ { dom 𝑈 } ) ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) )
197 106 196 syl5eq ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( 𝑍 ↾ suc dom 𝑈 ) = ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) )
198 197 breq2d ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ( ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) ↔ ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) ) )
199 102 198 mtbird ⊢ ( ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) ∧ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )
200 nosepssdm ⊢ ( ( 𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 )
201 7 35 120 200 syl3anc ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 )
202 nosepon ⊢ ( ( 𝑈 ∈ No ∧ 𝑍 ∈ No ∧ 𝑈 ≠ 𝑍 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On )
203 7 35 120 202 syl3anc ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On )
204 onsseleq ⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ On ∧ dom 𝑈 ∈ On ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 ↔ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) )
205 203 9 204 syl2anc ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ⊆ dom 𝑈 ↔ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) ) )
206 201 205 mpbid ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } ∈ dom 𝑈 ∨ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑍 ‘ 𝑥 ) } = dom 𝑈 ) )
207 99 199 206 mpjaodan ⊢ ( ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) ∧ 𝑍 <s 𝑈 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )
208 4 207 mpdan ⊢ ( ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈 ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀ 𝑏 ∈ 𝐵 𝑍 <s 𝑏 ) → ¬ ( 𝑈 ∪ { ⟨ dom 𝑈 , 1o ⟩ } ) <s ( 𝑍 ↾ suc dom 𝑈 ) )