Metamath Proof Explorer

Theorem nosupbday

Description: Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 nosupbday.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
3 2 adantr ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → 𝑆 ∈ No )
4 bdayval ⊢ ( 𝑆 ∈ No → ( bday ‘ 𝑆 ) = dom 𝑆 )
5 3 4 syl ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑆 ) = dom 𝑆 )
6 iftrue ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
7 1 6 syl5eq ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
8 7 dmeqd ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) )
9 2oex ⊢ 2o ∈ V
10 9 dmsnop ⊢ dom { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } = { dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) }
11 10 uneq2i ⊢ ( dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ dom { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) } )
12 dmun ⊢ dom ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ dom { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } )
13 df-suc ⊢ suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) = ( dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) } )
14 11 12 13 3eqtr4i ⊢ dom ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
15 8 14 eqtrdi ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
16 15 adantr ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → dom 𝑆 = suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
17 simprrl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → 𝑂 ∈ On )
18 eloni ⊢ ( 𝑂 ∈ On → Ord 𝑂 )
19 17 18 syl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → Ord 𝑂 )
20 simprll ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → 𝐴 ⊆ No )
21 simpl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
22 nomaxmo ⊢ ( 𝐴 ⊆ No → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
23 22 adantr ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
24 23 adantl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
25 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
26 21 24 25 sylanbrc ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
27 26 adantrr ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
28 riotacl ⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ 𝐴 )
29 27 28 syl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ 𝐴 )
30 20 29 sseldd ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ No )
31 bdayval ⊢ ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ No → ( bday ‘ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ) = dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
32 30 31 syl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ) = dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
33 simprrr ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( bday “ 𝐴 ) ⊆ 𝑂 )
34 bdayfo ⊢ bday : No –onto→ On
35 fofn ⊢ ( bday : No –onto→ On → bday Fn No )
36 34 35 ax-mp ⊢ bday Fn No
37 fnfvima ⊢ ( ( bday Fn No ∧ 𝐴 ⊆ No ∧ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ 𝐴 ) → ( bday ‘ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ) ∈ ( bday “ 𝐴 ) )
38 36 20 29 37 mp3an2i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ) ∈ ( bday “ 𝐴 ) )
39 33 38 sseldd ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ) ∈ 𝑂 )
40 32 39 eqeltrrd ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ 𝑂 )
41 ordsucss ⊢ ( Ord 𝑂 → ( dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∈ 𝑂 → suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ⊆ 𝑂 ) )
42 19 40 41 sylc ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → suc dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ⊆ 𝑂 )
43 16 42 eqsstrd ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → dom 𝑆 ⊆ 𝑂 )
44 iffalse ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
45 1 44 syl5eq ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
46 45 dmeqd ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
47 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ∈ V
48 eqid ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
49 47 48 dmmpti ⊢ dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
50 46 49 eqtrdi ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
51 50 adantr ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → dom 𝑆 = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
52 simplrl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑂 ∈ On )
53 ssel2 ⊢ ( ( 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ No )
54 53 ad4ant14 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ No )
55 bdayval ⊢ ( 𝑢 ∈ No → ( bday ‘ 𝑢 ) = dom 𝑢 )
56 54 55 syl ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( bday ‘ 𝑢 ) = dom 𝑢 )
57 simplrr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( bday “ 𝐴 ) ⊆ 𝑂 )
58 fnfvima ⊢ ( ( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴 ) → ( bday ‘ 𝑢 ) ∈ ( bday “ 𝐴 ) )
59 36 58 mp3an1 ⊢ ( ( 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴 ) → ( bday ‘ 𝑢 ) ∈ ( bday “ 𝐴 ) )
60 59 ad4ant14 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( bday ‘ 𝑢 ) ∈ ( bday “ 𝐴 ) )
61 57 60 sseldd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( bday ‘ 𝑢 ) ∈ 𝑂 )
62 56 61 eqeltrrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → dom 𝑢 ∈ 𝑂 )
63 onelss ⊢ ( 𝑂 ∈ On → ( dom 𝑢 ∈ 𝑂 → dom 𝑢 ⊆ 𝑂 ) )
64 52 62 63 sylc ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → dom 𝑢 ⊆ 𝑂 )
65 64 sseld ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑦 ∈ dom 𝑢 → 𝑦 ∈ 𝑂 ) )
66 65 adantrd ⊢ ( ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) → 𝑦 ∈ 𝑂 ) )
67 66 rexlimdva ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) → 𝑦 ∈ 𝑂 ) )
68 67 abssdv ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ 𝑂 )
69 68 adantl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ 𝑂 )
70 51 69 eqsstrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) ) → dom 𝑆 ⊆ 𝑂 )
71 43 70 pm2.61ian ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → dom 𝑆 ⊆ 𝑂 )
72 5 71 eqsstrd ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑂 ∈ On ∧ ( bday “ 𝐴 ) ⊆ 𝑂 ) ) → ( bday ‘ 𝑆 ) ⊆ 𝑂 )