Metamath Proof Explorer

Theorem noinfbday

Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024)

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

Proof

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