Metamath Proof Explorer

Theorem noinfbnd1lem5

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not 2o . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd1.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion noinfbnd1lem5 ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 1 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) → 𝑇 ∈ No )
3 2 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → 𝑇 ∈ No )
4 3 adantl ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → 𝑇 ∈ No )
5 nodmord ⊢ ( 𝑇 ∈ No → Ord dom 𝑇 )
6 4 5 syl ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → Ord dom 𝑇 )
7 ordirr ⊢ ( Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇 )
8 6 7 syl ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ dom 𝑇 ∈ dom 𝑇 )
9 simpr3l ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → 𝑈 ∈ 𝐵 )
10 9 adantr ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → 𝑈 ∈ 𝐵 )
11 ndmfv ⊢ ( ¬ dom 𝑇 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑇 ) = ∅ )
12 2on0 ⊢ 2o ≠ ∅
13 12 necomi ⊢ ∅ ≠ 2o
14 neeq1 ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = ∅ → ( ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ↔ ∅ ≠ 2o ) )
15 13 14 mpbiri ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = ∅ → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
16 11 15 syl ⊢ ( ¬ dom 𝑇 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
17 16 neneqd ⊢ ( ¬ dom 𝑇 ∈ dom 𝑈 → ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o )
18 17 con4i ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = 2o → dom 𝑇 ∈ dom 𝑈 )
19 18 adantl ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → dom 𝑇 ∈ dom 𝑈 )
20 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → 𝐵 ⊆ No )
21 20 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → 𝐵 ⊆ No )
22 simpl3l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → 𝑈 ∈ 𝐵 )
23 22 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → 𝑈 ∈ 𝐵 )
24 21 23 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → 𝑈 ∈ No )
25 nofun ⊢ ( 𝑈 ∈ No → Fun 𝑈 )
26 24 25 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → Fun 𝑈 )
27 simprll ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → 𝑧 ∈ 𝐵 )
28 21 27 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → 𝑧 ∈ No )
29 nofun ⊢ ( 𝑧 ∈ No → Fun 𝑧 )
30 28 29 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → Fun 𝑧 )
31 simpl3r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
32 31 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
33 simpll1 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
34 simpll2 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) )
35 simpll3 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) )
36 simprl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) )
37 1 noinfbnd1lem2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ) ) → ( 𝑧 ↾ dom 𝑇 ) = 𝑇 )
38 33 34 35 36 37 syl112anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑧 ↾ dom 𝑇 ) = 𝑇 )
39 32 38 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ↾ dom 𝑇 ) = ( 𝑧 ↾ dom 𝑇 ) )
40 simplr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ‘ dom 𝑇 ) = 2o )
41 40 18 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → dom 𝑇 ∈ dom 𝑈 )
42 simprr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑧 ‘ dom 𝑇 ) = 2o )
43 ndmfv ⊢ ( ¬ dom 𝑇 ∈ dom 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = ∅ )
44 neeq1 ⊢ ( ( 𝑧 ‘ dom 𝑇 ) = ∅ → ( ( 𝑧 ‘ dom 𝑇 ) ≠ 2o ↔ ∅ ≠ 2o ) )
45 13 44 mpbiri ⊢ ( ( 𝑧 ‘ dom 𝑇 ) = ∅ → ( 𝑧 ‘ dom 𝑇 ) ≠ 2o )
46 43 45 syl ⊢ ( ¬ dom 𝑇 ∈ dom 𝑧 → ( 𝑧 ‘ dom 𝑇 ) ≠ 2o )
47 46 neneqd ⊢ ( ¬ dom 𝑇 ∈ dom 𝑧 → ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o )
48 47 con4i ⊢ ( ( 𝑧 ‘ dom 𝑇 ) = 2o → dom 𝑇 ∈ dom 𝑧 )
49 42 48 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → dom 𝑇 ∈ dom 𝑧 )
50 40 42 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ‘ dom 𝑇 ) = ( 𝑧 ‘ dom 𝑇 ) )
51 eqfunressuc ⊢ ( ( ( Fun 𝑈 ∧ Fun 𝑧 ) ∧ ( 𝑈 ↾ dom 𝑇 ) = ( 𝑧 ↾ dom 𝑇 ) ∧ ( dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ ( 𝑈 ‘ dom 𝑇 ) = ( 𝑧 ‘ dom 𝑇 ) ) ) → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) )
52 26 30 39 41 49 50 51 syl213anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) )
53 52 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ) → ( ( 𝑧 ‘ dom 𝑇 ) = 2o → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) )
54 53 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ 𝑧 ∈ 𝐵 ) → ( ¬ 𝑈 <s 𝑧 → ( ( 𝑧 ‘ dom 𝑇 ) = 2o → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
55 54 a2d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) → ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
56 55 ralimdva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) → ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
57 56 impcom ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ) → ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) )
58 57 anassrs ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) )
59 dmeq ⊢ ( 𝑝 = 𝑈 → dom 𝑝 = dom 𝑈 )
60 59 eleq2d ⊢ ( 𝑝 = 𝑈 → ( dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈 ) )
61 breq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 <s 𝑧 ↔ 𝑈 <s 𝑧 ) )
62 61 notbid ⊢ ( 𝑝 = 𝑈 → ( ¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧 ) )
63 reseq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑈 ↾ suc dom 𝑇 ) )
64 63 eqeq1d ⊢ ( 𝑝 = 𝑈 → ( ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ↔ ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) )
65 62 64 imbi12d ⊢ ( 𝑝 = 𝑈 → ( ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ↔ ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
66 65 ralbidv ⊢ ( 𝑝 = 𝑈 → ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
67 60 66 anbi12d ⊢ ( 𝑝 = 𝑈 → ( ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ↔ ( dom 𝑇 ∈ dom 𝑈 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) )
68 67 rspcev ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ( dom 𝑇 ∈ dom 𝑈 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) → ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
69 10 19 58 68 syl12anc ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
70 nodmon ⊢ ( 𝑇 ∈ No → dom 𝑇 ∈ On )
71 4 70 syl ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → dom 𝑇 ∈ On )
72 71 adantr ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → dom 𝑇 ∈ On )
73 eleq1 ⊢ ( 𝑎 = dom 𝑇 → ( 𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝 ) )
74 suceq ⊢ ( 𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇 )
75 74 reseq2d ⊢ ( 𝑎 = dom 𝑇 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑝 ↾ suc dom 𝑇 ) )
76 74 reseq2d ⊢ ( 𝑎 = dom 𝑇 → ( 𝑧 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc dom 𝑇 ) )
77 75 76 eqeq12d ⊢ ( 𝑎 = dom 𝑇 → ( ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ↔ ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) )
78 77 imbi2d ⊢ ( 𝑎 = dom 𝑇 → ( ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ↔ ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
79 78 ralbidv ⊢ ( 𝑎 = dom 𝑇 → ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) )
80 73 79 anbi12d ⊢ ( 𝑎 = dom 𝑇 → ( ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) ↔ ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) )
81 80 rexbidv ⊢ ( 𝑎 = dom 𝑇 → ( ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) )
82 81 elabg ⊢ ( dom 𝑇 ∈ On → ( dom 𝑇 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) )
83 72 82 syl ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ( dom 𝑇 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑧 ↾ suc dom 𝑇 ) ) ) ) )
84 69 83 mpbird ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → dom 𝑇 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
85 1 noinfdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
86 85 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → dom 𝑇 = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
87 86 adantl ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → dom 𝑇 = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
88 87 adantr ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → dom 𝑇 = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
89 88 eleq2d ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → ( dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑝 <s 𝑧 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ) )
90 84 89 mpbird ⊢ ( ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 2o ) → dom 𝑇 ∈ dom 𝑇 )
91 8 90 mtand ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o )
92 91 neqned ⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
93 rexanali ⊢ ( ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ↔ ¬ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) )
94 simpr1 ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
95 simpr2 ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) )
96 simplll ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → 𝑧 ∈ 𝐵 )
97 simpr3 ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) )
98 simpll ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) )
99 94 95 97 98 37 syl112anc ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑧 ↾ dom 𝑇 ) = 𝑇 )
100 1 noinfbnd1lem4 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑧 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑧 ‘ dom 𝑇 ) ≠ ∅ )
101 94 95 96 99 100 syl112anc ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑧 ‘ dom 𝑇 ) ≠ ∅ )
102 101 neneqd ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ ( 𝑧 ‘ dom 𝑇 ) = ∅ )
103 102 pm2.21d ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( ( 𝑧 ‘ dom 𝑇 ) = ∅ → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ) )
104 1 noinfbnd1lem3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑧 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑧 ‘ dom 𝑇 ) ≠ 1o )
105 94 95 96 99 104 syl112anc ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑧 ‘ dom 𝑇 ) ≠ 1o )
106 105 neneqd ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ ( 𝑧 ‘ dom 𝑇 ) = 1o )
107 106 pm2.21d ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( ( 𝑧 ‘ dom 𝑇 ) = 1o → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ) )
108 simplr ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o )
109 simpr2l ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → 𝐵 ⊆ No )
110 109 96 sseldd ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → 𝑧 ∈ No )
111 nofv ⊢ ( 𝑧 ∈ No → ( ( 𝑧 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑇 ) = 1o ∨ ( 𝑧 ‘ dom 𝑇 ) = 2o ) )
112 110 111 syl ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( ( 𝑧 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑇 ) = 1o ∨ ( 𝑧 ‘ dom 𝑇 ) = 2o ) )
113 3orel3 ⊢ ( ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o → ( ( ( 𝑧 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑇 ) = 1o ∨ ( 𝑧 ‘ dom 𝑇 ) = 2o ) → ( ( 𝑧 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑇 ) = 1o ) ) )
114 108 112 113 sylc ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( ( 𝑧 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑇 ) = 1o ) )
115 103 107 114 mpjaod ⊢ ( ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
116 115 ex ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧 ) ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) → ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ) )
117 116 anasss ⊢ ( ( 𝑧 ∈ 𝐵 ∧ ( ¬ 𝑈 <s 𝑧 ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ) → ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ) )
118 117 rexlimiva ⊢ ( ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) → ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o ) )
119 118 imp ⊢ ( ( ∃ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 ∧ ¬ ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
120 93 119 sylanbr ⊢ ( ( ¬ ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑈 <s 𝑧 → ( 𝑧 ‘ dom 𝑇 ) = 2o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
121 92 120 pm2.61ian ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )