Metamath Proof Explorer


Theorem noinfbnd1lem4

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not undefined. (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 noinfbnd1lem4 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 simpl1 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
3 simpl2 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝐵 No 𝐵𝑉 ) )
4 simprl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑤𝐵 )
5 simpl3 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) )
6 simp2l ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → 𝐵 No )
7 6 sselda ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ 𝑤𝐵 ) → 𝑤 No )
8 simp3l ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → 𝑈𝐵 )
9 6 8 sseldd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → 𝑈 No )
10 9 adantr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ 𝑤𝐵 ) → 𝑈 No )
11 sltso <s Or No
12 soasym ( ( <s Or No ∧ ( 𝑤 No 𝑈 No ) ) → ( 𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤 ) )
13 11 12 mpan ( ( 𝑤 No 𝑈 No ) → ( 𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤 ) )
14 7 10 13 syl2anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ 𝑤𝐵 ) → ( 𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤 ) )
15 14 impr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ¬ 𝑈 <s 𝑤 )
16 4 15 jca ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤 ) )
17 1 noinfbnd1lem2 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤 ) ) ) → ( 𝑤 ↾ dom 𝑇 ) = 𝑇 )
18 2 3 5 16 17 syl112anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 ↾ dom 𝑇 ) = 𝑇 )
19 1 noinfbnd1lem3 ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑤𝐵 ∧ ( 𝑤 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑤 ‘ dom 𝑇 ) ≠ 1o )
20 2 3 4 18 19 syl112anc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 ‘ dom 𝑇 ) ≠ 1o )
21 20 neneqd ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ¬ ( 𝑤 ‘ dom 𝑇 ) = 1o )
22 21 expr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ 𝑤𝐵 ) → ( 𝑤 <s 𝑈 → ¬ ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
23 imnan ( ( 𝑤 <s 𝑈 → ¬ ( 𝑤 ‘ dom 𝑇 ) = 1o ) ↔ ¬ ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
24 22 23 sylib ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ 𝑤𝐵 ) → ¬ ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
25 24 nrexdv ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ¬ ∃ 𝑤𝐵 ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
26 breq2 ( 𝑥 = 𝑈 → ( 𝑦 <s 𝑥𝑦 <s 𝑈 ) )
27 26 rexbidv ( 𝑥 = 𝑈 → ( ∃ 𝑦𝐵 𝑦 <s 𝑥 ↔ ∃ 𝑦𝐵 𝑦 <s 𝑈 ) )
28 simpl1 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
29 dfral2 ( ∀ 𝑥𝐵𝑦𝐵 𝑦 <s 𝑥 ↔ ¬ ∃ 𝑥𝐵 ¬ ∃ 𝑦𝐵 𝑦 <s 𝑥 )
30 ralnex ( ∀ 𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ¬ ∃ 𝑦𝐵 𝑦 <s 𝑥 )
31 30 rexbii ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ∃ 𝑥𝐵 ¬ ∃ 𝑦𝐵 𝑦 <s 𝑥 )
32 29 31 xchbinxr ( ∀ 𝑥𝐵𝑦𝐵 𝑦 <s 𝑥 ↔ ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
33 28 32 sylibr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ∀ 𝑥𝐵𝑦𝐵 𝑦 <s 𝑥 )
34 simpl3l ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → 𝑈𝐵 )
35 27 33 34 rspcdva ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ∃ 𝑦𝐵 𝑦 <s 𝑈 )
36 breq1 ( 𝑦 = 𝑤 → ( 𝑦 <s 𝑈𝑤 <s 𝑈 ) )
37 36 cbvrexvw ( ∃ 𝑦𝐵 𝑦 <s 𝑈 ↔ ∃ 𝑤𝐵 𝑤 <s 𝑈 )
38 35 37 sylib ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ∃ 𝑤𝐵 𝑤 <s 𝑈 )
39 simpl2l ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → 𝐵 No )
40 39 adantr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝐵 No )
41 simprl ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑤𝐵 )
42 40 41 sseldd ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑤 No )
43 34 adantr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑈𝐵 )
44 40 43 sseldd ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑈 No )
45 simpl2 ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ( 𝐵 No 𝐵𝑉 ) )
46 1 noinfno ( ( 𝐵 No 𝐵𝑉 ) → 𝑇 No )
47 45 46 syl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → 𝑇 No )
48 47 adantr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑇 No )
49 nodmon ( 𝑇 No → dom 𝑇 ∈ On )
50 48 49 syl ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → dom 𝑇 ∈ On )
51 simpll1 ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
52 simpll2 ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝐵 No 𝐵𝑉 ) )
53 simpll3 ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) )
54 simprr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → 𝑤 <s 𝑈 )
55 42 44 13 syl2anc ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤 ) )
56 54 55 mpd ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ¬ 𝑈 <s 𝑤 )
57 41 56 jca ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤 ) )
58 51 52 53 57 17 syl112anc ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 ↾ dom 𝑇 ) = 𝑇 )
59 simpl3r ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
60 59 adantr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
61 58 60 eqtr4d ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 ↾ dom 𝑇 ) = ( 𝑈 ↾ dom 𝑇 ) )
62 simplr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑈 ‘ dom 𝑇 ) = ∅ )
63 nogt01o ( ( ( 𝑤 No 𝑈 No ∧ dom 𝑇 ∈ On ) ∧ ( ( 𝑤 ↾ dom 𝑇 ) = ( 𝑈 ↾ dom 𝑇 ) ∧ 𝑤 <s 𝑈 ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ( 𝑤 ‘ dom 𝑇 ) = 1o )
64 42 44 50 61 54 62 63 syl321anc ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ ( 𝑤𝐵𝑤 <s 𝑈 ) ) → ( 𝑤 ‘ dom 𝑇 ) = 1o )
65 64 expr ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ 𝑤𝐵 ) → ( 𝑤 <s 𝑈 → ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
66 65 ancld ( ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) ∧ 𝑤𝐵 ) → ( 𝑤 <s 𝑈 → ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) ) )
67 66 reximdva ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ( ∃ 𝑤𝐵 𝑤 <s 𝑈 → ∃ 𝑤𝐵 ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) ) )
68 38 67 mpd ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = ∅ ) → ∃ 𝑤𝐵 ( 𝑤 <s 𝑈 ∧ ( 𝑤 ‘ dom 𝑇 ) = 1o ) )
69 25 68 mtand ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = ∅ )
70 69 neqned ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ∧ ( 𝑈𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ ∅ )