Metamath Proof Explorer

Theorem nosupbnd1lem3

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not 2o . (Contributed by Scott Fenton, 6-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 nosupbnd1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
3 2 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑆 ∈ No )
4 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
5 ordirr ⊢ ( Ord dom 𝑆 → ¬ dom 𝑆 ∈ dom 𝑆 )
6 3 4 5 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ dom 𝑆 ∈ dom 𝑆 )
7 simpl3l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → 𝑈 ∈ 𝐴 )
8 ndmfv ⊢ ( ¬ dom 𝑆 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑆 ) = ∅ )
9 2on ⊢ 2o ∈ On
10 9 elexi ⊢ 2o ∈ V
11 10 prid2 ⊢ 2o ∈ { 1o , 2o }
12 11 nosgnn0i ⊢ ∅ ≠ 2o
13 neeq1 ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ( ( 𝑈 ‘ dom 𝑆 ) ≠ 2o ↔ ∅ ≠ 2o ) )
14 12 13 mpbiri ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ( 𝑈 ‘ dom 𝑆 ) ≠ 2o )
15 14 neneqd ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ¬ ( 𝑈 ‘ dom 𝑆 ) = 2o )
16 8 15 syl ⊢ ( ¬ dom 𝑆 ∈ dom 𝑈 → ¬ ( 𝑈 ‘ dom 𝑆 ) = 2o )
17 16 con4i ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = 2o → dom 𝑆 ∈ dom 𝑈 )
18 17 adantl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → dom 𝑆 ∈ dom 𝑈 )
19 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → 𝐴 ⊆ No )
20 19 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝐴 ⊆ No )
21 7 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝑈 ∈ 𝐴 )
22 20 21 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝑈 ∈ No )
23 simprl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝑞 ∈ 𝐴 )
24 20 23 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝑞 ∈ No )
25 3 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → 𝑆 ∈ No )
26 25 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → 𝑆 ∈ No )
27 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
28 26 27 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → dom 𝑆 ∈ On )
29 simpl3r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
30 29 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
31 simpll1 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
32 simpll2 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
33 simpll3 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) )
34 simpr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) )
35 1 nosupbnd1lem2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) ) → ( 𝑞 ↾ dom 𝑆 ) = 𝑆 )
36 31 32 33 34 35 syl112anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑞 ↾ dom 𝑆 ) = 𝑆 )
37 30 36 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑈 ↾ dom 𝑆 ) = ( 𝑞 ↾ dom 𝑆 ) )
38 simplr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑈 ‘ dom 𝑆 ) = 2o )
39 simprr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ¬ 𝑞 <s 𝑈 )
40 nolesgn2ores ⊢ ( ( ( 𝑈 ∈ No ∧ 𝑞 ∈ No ∧ dom 𝑆 ∈ On ) ∧ ( ( 𝑈 ↾ dom 𝑆 ) = ( 𝑞 ↾ dom 𝑆 ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ¬ 𝑞 <s 𝑈 ) → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) )
41 22 24 28 37 38 39 40 syl321anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 <s 𝑈 ) ) → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) )
42 41 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) )
43 42 ralrimiva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) )
44 dmeq ⊢ ( 𝑝 = 𝑈 → dom 𝑝 = dom 𝑈 )
45 44 eleq2d ⊢ ( 𝑝 = 𝑈 → ( dom 𝑆 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑈 ) )
46 breq2 ⊢ ( 𝑝 = 𝑈 → ( 𝑞 <s 𝑝 ↔ 𝑞 <s 𝑈 ) )
47 46 notbid ⊢ ( 𝑝 = 𝑈 → ( ¬ 𝑞 <s 𝑝 ↔ ¬ 𝑞 <s 𝑈 ) )
48 reseq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑈 ↾ suc dom 𝑆 ) )
49 48 eqeq1d ⊢ ( 𝑝 = 𝑈 → ( ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ↔ ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) )
50 47 49 imbi12d ⊢ ( 𝑝 = 𝑈 → ( ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ↔ ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
51 50 ralbidv ⊢ ( 𝑝 = 𝑈 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
52 45 51 anbi12d ⊢ ( 𝑝 = 𝑈 → ( ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ↔ ( dom 𝑆 ∈ dom 𝑈 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
53 52 rspcev ⊢ ( ( 𝑈 ∈ 𝐴 ∧ ( dom 𝑆 ∈ dom 𝑈 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
54 7 18 43 53 syl12anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
55 1 nosupdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } )
56 55 eleq2d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ) )
57 56 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ) )
58 eleq1 ⊢ ( 𝑧 = dom 𝑆 → ( 𝑧 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑝 ) )
59 suceq ⊢ ( 𝑧 = dom 𝑆 → suc 𝑧 = suc dom 𝑆 )
60 59 reseq2d ⊢ ( 𝑧 = dom 𝑆 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑝 ↾ suc dom 𝑆 ) )
61 59 reseq2d ⊢ ( 𝑧 = dom 𝑆 → ( 𝑞 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc dom 𝑆 ) )
62 60 61 eqeq12d ⊢ ( 𝑧 = dom 𝑆 → ( ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ↔ ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) )
63 62 imbi2d ⊢ ( 𝑧 = dom 𝑆 → ( ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ↔ ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
64 63 ralbidv ⊢ ( 𝑧 = dom 𝑆 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) )
65 58 64 anbi12d ⊢ ( 𝑧 = dom 𝑆 → ( ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ↔ ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
66 65 rexbidv ⊢ ( 𝑧 = dom 𝑆 → ( ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
67 66 elabg ⊢ ( dom 𝑆 ∈ On → ( dom 𝑆 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
68 3 27 67 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( dom 𝑆 ∈ { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
69 57 68 bitrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( dom 𝑆 ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
70 69 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → ( dom 𝑆 ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑞 ↾ suc dom 𝑆 ) ) ) ) )
71 54 70 mpbird ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 2o ) → dom 𝑆 ∈ dom 𝑆 )
72 6 71 mtand ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ ( 𝑈 ‘ dom 𝑆 ) = 2o )
73 72 neqned ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 2o )