Metamath Proof Explorer

Theorem noinfbnd1lem3

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

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 nodmord ⊢ ( 𝑇 ∈ No → Ord dom 𝑇 )
5 ordirr ⊢ ( Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇 )
6 3 4 5 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ¬ dom 𝑇 ∈ dom 𝑇 )
7 simpl3l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → 𝑈 ∈ 𝐵 )
8 ndmfv ⊢ ( ¬ dom 𝑇 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑇 ) = ∅ )
9 1n0 ⊢ 1o ≠ ∅
10 9 necomi ⊢ ∅ ≠ 1o
11 neeq1 ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = ∅ → ( ( 𝑈 ‘ dom 𝑇 ) ≠ 1o ↔ ∅ ≠ 1o ) )
12 10 11 mpbiri ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = ∅ → ( 𝑈 ‘ dom 𝑇 ) ≠ 1o )
13 12 neneqd ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = ∅ → ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o )
14 8 13 syl ⊢ ( ¬ dom 𝑇 ∈ dom 𝑈 → ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o )
15 14 con4i ⊢ ( ( 𝑈 ‘ dom 𝑇 ) = 1o → dom 𝑇 ∈ dom 𝑈 )
16 15 adantl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → dom 𝑇 ∈ dom 𝑈 )
17 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → 𝐵 ⊆ No )
18 17 7 sseldd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → 𝑈 ∈ No )
19 18 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → 𝑈 ∈ No )
20 17 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → 𝐵 ⊆ No )
21 simprl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → 𝑞 ∈ 𝐵 )
22 20 21 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → 𝑞 ∈ No )
23 3 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → 𝑇 ∈ No )
24 nodmon ⊢ ( 𝑇 ∈ No → dom 𝑇 ∈ On )
25 23 24 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → dom 𝑇 ∈ On )
26 25 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → dom 𝑇 ∈ On )
27 simpl3r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
28 27 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
29 simpll1 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
30 simpll2 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) )
31 simpll3 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) )
32 simpr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) )
33 1 noinfbnd1lem2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) ) → ( 𝑞 ↾ dom 𝑇 ) = 𝑇 )
34 29 30 31 32 33 syl112anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑞 ↾ dom 𝑇 ) = 𝑇 )
35 28 34 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑈 ↾ dom 𝑇 ) = ( 𝑞 ↾ dom 𝑇 ) )
36 simplr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑈 ‘ dom 𝑇 ) = 1o )
37 simprr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ¬ 𝑈 <s 𝑞 )
38 nogesgn1ores ⊢ ( ( ( 𝑈 ∈ No ∧ 𝑞 ∈ No ∧ dom 𝑇 ∈ On ) ∧ ( ( 𝑈 ↾ dom 𝑇 ) = ( 𝑞 ↾ dom 𝑇 ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ¬ 𝑈 <s 𝑞 ) → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) )
39 19 22 26 35 36 37 38 syl321anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ ( 𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞 ) ) → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) )
40 39 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) ∧ 𝑞 ∈ 𝐵 ) → ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) )
41 40 ralrimiva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) )
42 dmeq ⊢ ( 𝑝 = 𝑈 → dom 𝑝 = dom 𝑈 )
43 42 eleq2d ⊢ ( 𝑝 = 𝑈 → ( dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈 ) )
44 breq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 <s 𝑞 ↔ 𝑈 <s 𝑞 ) )
45 44 notbid ⊢ ( 𝑝 = 𝑈 → ( ¬ 𝑝 <s 𝑞 ↔ ¬ 𝑈 <s 𝑞 ) )
46 reseq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑈 ↾ suc dom 𝑇 ) )
47 46 eqeq1d ⊢ ( 𝑝 = 𝑈 → ( ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ↔ ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) )
48 45 47 imbi12d ⊢ ( 𝑝 = 𝑈 → ( ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ↔ ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
49 48 ralbidv ⊢ ( 𝑝 = 𝑈 → ( ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ↔ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
50 43 49 anbi12d ⊢ ( 𝑝 = 𝑈 → ( ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ↔ ( dom 𝑇 ∈ dom 𝑈 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
51 50 rspcev ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ( dom 𝑇 ∈ dom 𝑈 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑈 <s 𝑞 → ( 𝑈 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) → ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
52 7 16 41 51 syl12anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
53 1 noinfdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { 𝑧 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } )
54 53 eleq2d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ) )
55 54 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ) )
56 eleq1 ⊢ ( 𝑧 = dom 𝑇 → ( 𝑧 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝 ) )
57 suceq ⊢ ( 𝑧 = dom 𝑇 → suc 𝑧 = suc dom 𝑇 )
58 57 reseq2d ⊢ ( 𝑧 = dom 𝑇 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑝 ↾ suc dom 𝑇 ) )
59 57 reseq2d ⊢ ( 𝑧 = dom 𝑇 → ( 𝑞 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc dom 𝑇 ) )
60 58 59 eqeq12d ⊢ ( 𝑧 = dom 𝑇 → ( ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ↔ ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) )
61 60 imbi2d ⊢ ( 𝑧 = dom 𝑇 → ( ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ↔ ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
62 61 ralbidv ⊢ ( 𝑧 = dom 𝑇 → ( ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ↔ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) )
63 56 62 anbi12d ⊢ ( 𝑧 = dom 𝑇 → ( ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ↔ ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
64 63 rexbidv ⊢ ( 𝑧 = dom 𝑇 → ( ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
65 64 elabg ⊢ ( dom 𝑇 ∈ On → ( dom 𝑇 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
66 3 24 65 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( dom 𝑇 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐵 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
67 55 66 bitrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( dom 𝑇 ∈ dom 𝑇 ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
68 67 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → ( dom 𝑇 ∈ dom 𝑇 ↔ ∃ 𝑝 ∈ 𝐵 ( dom 𝑇 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐵 ( ¬ 𝑝 <s 𝑞 → ( 𝑝 ↾ suc dom 𝑇 ) = ( 𝑞 ↾ suc dom 𝑇 ) ) ) ) )
69 52 68 mpbird ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) ∧ ( 𝑈 ‘ dom 𝑇 ) = 1o ) → dom 𝑇 ∈ dom 𝑇 )
70 6 69 mtand ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o )
71 70 neqned ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 1o )