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 )