Metamath Proof Explorer


Theorem noinfno

Description: The next several theorems deal with a surreal "infimum". This surreal will ultimately be shown to bound B above and bound the restriction of any surreal below. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 8-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 noinfno.1 𝑇 = if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 iftrue ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
3 2 adantr ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) )
4 simprl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → 𝐵 No )
5 simpl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
6 nominmo ( 𝐵 No → ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
7 6 ad2antrl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
8 reu5 ( ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃* 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) )
9 5 7 8 sylanbrc ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 )
10 riotacl ( ∃! 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ 𝐵 )
11 9 10 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ 𝐵 )
12 4 11 sseldd ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No )
13 1oex 1o ∈ V
14 13 prid1 1o ∈ { 1o , 2o }
15 14 noextend ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∈ No → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No )
16 12 15 syl ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) ∈ No )
17 3 16 eqeltrd ( ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) ∈ No )
18 iffalse ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
19 18 adantr ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
20 funmpt Fun ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
21 20 a1i ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → Fun ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
22 iotaex ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ∈ V
23 eqid ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
24 22 23 dmmpti dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
25 simpl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝐵 No )
26 simprl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝑢𝐵 )
27 25 26 sseldd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝑢 No )
28 nodmon ( 𝑢 No → dom 𝑢 ∈ On )
29 27 28 syl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → dom 𝑢 ∈ On )
30 simprrl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝑦 ∈ dom 𝑢 )
31 onelon ( ( dom 𝑢 ∈ On ∧ 𝑦 ∈ dom 𝑢 ) → 𝑦 ∈ On )
32 29 30 31 syl2anc ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝑦 ∈ On )
33 32 rexlimdvaa ( 𝐵 No → ( ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) → 𝑦 ∈ On ) )
34 33 abssdv ( 𝐵 No → { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ On )
35 simplr ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → 𝑎𝑏 )
36 ssel2 ( ( 𝐵 No 𝑢𝐵 ) → 𝑢 No )
37 36 adantlr ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → 𝑢 No )
38 37 28 syl ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → dom 𝑢 ∈ On )
39 ontr1 ( dom 𝑢 ∈ On → ( ( 𝑎𝑏𝑏 ∈ dom 𝑢 ) → 𝑎 ∈ dom 𝑢 ) )
40 38 39 syl ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → ( ( 𝑎𝑏𝑏 ∈ dom 𝑢 ) → 𝑎 ∈ dom 𝑢 ) )
41 35 40 mpand ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → ( 𝑏 ∈ dom 𝑢𝑎 ∈ dom 𝑢 ) )
42 41 adantrd ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → ( ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) → 𝑎 ∈ dom 𝑢 ) )
43 reseq1 ( ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) → ( ( 𝑢 ↾ suc 𝑏 ) ↾ suc 𝑎 ) = ( ( 𝑣 ↾ suc 𝑏 ) ↾ suc 𝑎 ) )
44 onelon ( ( dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢 ) → 𝑏 ∈ On )
45 38 44 sylan ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → 𝑏 ∈ On )
46 sucelon ( 𝑏 ∈ On ↔ suc 𝑏 ∈ On )
47 45 46 sylib ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → suc 𝑏 ∈ On )
48 simpllr ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → 𝑎𝑏 )
49 eloni ( 𝑏 ∈ On → Ord 𝑏 )
50 45 49 syl ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → Ord 𝑏 )
51 ordsucelsuc ( Ord 𝑏 → ( 𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏 ) )
52 50 51 syl ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( 𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏 ) )
53 48 52 mpbid ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → suc 𝑎 ∈ suc 𝑏 )
54 onelss ( suc 𝑏 ∈ On → ( suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏 ) )
55 47 53 54 sylc ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → suc 𝑎 ⊆ suc 𝑏 )
56 55 resabs1d ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ( 𝑢 ↾ suc 𝑏 ) ↾ suc 𝑎 ) = ( 𝑢 ↾ suc 𝑎 ) )
57 55 resabs1d ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ( 𝑣 ↾ suc 𝑏 ) ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) )
58 56 57 eqeq12d ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ( ( 𝑢 ↾ suc 𝑏 ) ↾ suc 𝑎 ) = ( ( 𝑣 ↾ suc 𝑏 ) ↾ suc 𝑎 ) ↔ ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
59 43 58 syl5ib ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
60 59 imim2d ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) → ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
61 60 ralimdv ( ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) ∧ 𝑏 ∈ dom 𝑢 ) → ( ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) → ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
62 61 expimpd ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → ( ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) → ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
63 42 62 jcad ( ( ( 𝐵 No 𝑎𝑏 ) ∧ 𝑢𝐵 ) → ( ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) → ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) )
64 63 reximdva ( ( 𝐵 No 𝑎𝑏 ) → ( ∃ 𝑢𝐵 ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) → ∃ 𝑢𝐵 ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) )
65 64 expimpd ( 𝐵 No → ( ( 𝑎𝑏 ∧ ∃ 𝑢𝐵 ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) ) → ∃ 𝑢𝐵 ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) )
66 vex 𝑏 ∈ V
67 eleq1w ( 𝑦 = 𝑏 → ( 𝑦 ∈ dom 𝑢𝑏 ∈ dom 𝑢 ) )
68 suceq ( 𝑦 = 𝑏 → suc 𝑦 = suc 𝑏 )
69 68 reseq2d ( 𝑦 = 𝑏 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝑏 ) )
70 68 reseq2d ( 𝑦 = 𝑏 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑏 ) )
71 69 70 eqeq12d ( 𝑦 = 𝑏 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) )
72 71 imbi2d ( 𝑦 = 𝑏 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) )
73 72 ralbidv ( 𝑦 = 𝑏 → ( ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) )
74 67 73 anbi12d ( 𝑦 = 𝑏 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) ) )
75 74 rexbidv ( 𝑦 = 𝑏 → ( ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢𝐵 ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) ) )
76 66 75 elab ( 𝑏 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑢𝐵 ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) )
77 76 anbi2i ( ( 𝑎𝑏𝑏 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) ↔ ( 𝑎𝑏 ∧ ∃ 𝑢𝐵 ( 𝑏 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑏 ) = ( 𝑣 ↾ suc 𝑏 ) ) ) ) )
78 vex 𝑎 ∈ V
79 eleq1w ( 𝑦 = 𝑎 → ( 𝑦 ∈ dom 𝑢𝑎 ∈ dom 𝑢 ) )
80 suceq ( 𝑦 = 𝑎 → suc 𝑦 = suc 𝑎 )
81 80 reseq2d ( 𝑦 = 𝑎 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝑎 ) )
82 80 reseq2d ( 𝑦 = 𝑎 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑎 ) )
83 81 82 eqeq12d ( 𝑦 = 𝑎 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
84 83 imbi2d ( 𝑦 = 𝑎 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
85 84 ralbidv ( 𝑦 = 𝑎 → ( ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
86 79 85 anbi12d ( 𝑦 = 𝑎 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) )
87 86 rexbidv ( 𝑦 = 𝑎 → ( ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢𝐵 ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) )
88 78 87 elab ( 𝑎 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑢𝐵 ( 𝑎 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
89 65 77 88 3imtr4g ( 𝐵 No → ( ( 𝑎𝑏𝑏 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) → 𝑎 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
90 89 alrimivv ( 𝐵 No → ∀ 𝑎𝑏 ( ( 𝑎𝑏𝑏 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) → 𝑎 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
91 dftr2 ( Tr { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∀ 𝑎𝑏 ( ( 𝑎𝑏𝑏 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) → 𝑎 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
92 90 91 sylibr ( 𝐵 No → Tr { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
93 dford5 ( Ord { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ( { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ On ∧ Tr { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
94 34 92 93 sylanbrc ( 𝐵 No → Ord { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
95 94 ad2antrl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → Ord { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
96 bdayfo bday : No onto→ On
97 fofun ( bday : No onto→ On → Fun bday )
98 96 97 ax-mp Fun bday
99 funimaexg ( ( Fun bday 𝐵𝑉 ) → ( bday 𝐵 ) ∈ V )
100 98 99 mpan ( 𝐵𝑉 → ( bday 𝐵 ) ∈ V )
101 100 uniexd ( 𝐵𝑉 ( bday 𝐵 ) ∈ V )
102 101 adantl ( ( 𝐵 No 𝐵𝑉 ) → ( bday 𝐵 ) ∈ V )
103 102 adantl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( bday 𝐵 ) ∈ V )
104 bdayval ( 𝑢 No → ( bday 𝑢 ) = dom 𝑢 )
105 27 104 syl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → ( bday 𝑢 ) = dom 𝑢 )
106 fofn ( bday : No onto→ On → bday Fn No )
107 96 106 ax-mp bday Fn No
108 fnfvima ( ( bday Fn No 𝐵 No 𝑢𝐵 ) → ( bday 𝑢 ) ∈ ( bday 𝐵 ) )
109 107 108 mp3an1 ( ( 𝐵 No 𝑢𝐵 ) → ( bday 𝑢 ) ∈ ( bday 𝐵 ) )
110 109 adantrr ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → ( bday 𝑢 ) ∈ ( bday 𝐵 ) )
111 105 110 eqeltrrd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → dom 𝑢 ∈ ( bday 𝐵 ) )
112 elssuni ( dom 𝑢 ∈ ( bday 𝐵 ) → dom 𝑢 ( bday 𝐵 ) )
113 111 112 syl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → dom 𝑢 ( bday 𝐵 ) )
114 113 30 sseldd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ) ) → 𝑦 ( bday 𝐵 ) )
115 114 rexlimdvaa ( 𝐵 No → ( ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) → 𝑦 ( bday 𝐵 ) ) )
116 115 abssdv ( 𝐵 No → { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ ( bday 𝐵 ) )
117 116 ad2antrl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ⊆ ( bday 𝐵 ) )
118 103 117 ssexd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ∈ V )
119 elong ( { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ∈ V → ( { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ∈ On ↔ Ord { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
120 118 119 syl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ∈ On ↔ Ord { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
121 95 120 mpbird ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ∈ On )
122 24 121 eqeltrid ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ∈ On )
123 23 rnmpt ran ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) = { 𝑧 ∣ ∃ 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) }
124 eleq1w ( 𝑦 = 𝑔 → ( 𝑦 ∈ dom 𝑢𝑔 ∈ dom 𝑢 ) )
125 suceq ( 𝑦 = 𝑔 → suc 𝑦 = suc 𝑔 )
126 125 reseq2d ( 𝑦 = 𝑔 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝑔 ) )
127 125 reseq2d ( 𝑦 = 𝑔 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑔 ) )
128 126 127 eqeq12d ( 𝑦 = 𝑔 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) )
129 128 imbi2d ( 𝑦 = 𝑔 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) )
130 129 ralbidv ( 𝑦 = 𝑔 → ( ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) )
131 124 130 anbi12d ( 𝑦 = 𝑔 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) )
132 131 rexbidv ( 𝑦 = 𝑔 → ( ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) )
133 132 rexab ( ∃ 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ↔ ∃ 𝑔 ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ∧ 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
134 eqid ( 𝑢𝑔 ) = ( 𝑢𝑔 )
135 fvex ( 𝑢𝑔 ) ∈ V
136 eqeq2 ( 𝑥 = ( 𝑢𝑔 ) → ( ( 𝑢𝑔 ) = 𝑥 ↔ ( 𝑢𝑔 ) = ( 𝑢𝑔 ) ) )
137 136 3anbi3d ( 𝑥 = ( 𝑢𝑔 ) → ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = ( 𝑢𝑔 ) ) ) )
138 135 137 spcev ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = ( 𝑢𝑔 ) ) → ∃ 𝑥 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
139 134 138 mp3an3 ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) → ∃ 𝑥 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
140 139 reximi ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) → ∃ 𝑢𝐵𝑥 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
141 rexcom4 ( ∃ 𝑢𝐵𝑥 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ∃ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
142 140 141 sylib ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) → ∃ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
143 142 adantl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ∃ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
144 noinfprefixmo ( 𝐵 No → ∃* 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
145 144 ad2antrl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ∃* 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
146 145 adantr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ∃* 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
147 df-eu ( ∃! 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ( ∃ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ∧ ∃* 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
148 143 146 147 sylanbrc ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ∃! 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) )
149 vex 𝑧 ∈ V
150 eqeq2 ( 𝑥 = 𝑧 → ( ( 𝑢𝑔 ) = 𝑥 ↔ ( 𝑢𝑔 ) = 𝑧 ) )
151 150 3anbi3d ( 𝑥 = 𝑧 → ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) )
152 151 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) )
153 152 iota2 ( ( 𝑧 ∈ V ∧ ∃! 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ↔ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) = 𝑧 ) )
154 149 153 mpan ( ∃! 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ↔ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) = 𝑧 ) )
155 148 154 syl ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ↔ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) = 𝑧 ) )
156 eqcom ( ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) = 𝑧𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
157 155 156 bitrdi ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ↔ 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
158 simprr3 ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → ( 𝑢𝑔 ) = 𝑧 )
159 simpl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → 𝐵 No )
160 simprl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → 𝑢𝐵 )
161 159 160 sseldd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → 𝑢 No )
162 norn ( 𝑢 No → ran 𝑢 ⊆ { 1o , 2o } )
163 161 162 syl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → ran 𝑢 ⊆ { 1o , 2o } )
164 nofun ( 𝑢 No → Fun 𝑢 )
165 161 164 syl ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → Fun 𝑢 )
166 simprr1 ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → 𝑔 ∈ dom 𝑢 )
167 fvelrn ( ( Fun 𝑢𝑔 ∈ dom 𝑢 ) → ( 𝑢𝑔 ) ∈ ran 𝑢 )
168 165 166 167 syl2anc ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → ( 𝑢𝑔 ) ∈ ran 𝑢 )
169 163 168 sseldd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → ( 𝑢𝑔 ) ∈ { 1o , 2o } )
170 158 169 eqeltrrd ( ( 𝐵 No ∧ ( 𝑢𝐵 ∧ ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) ) ) → 𝑧 ∈ { 1o , 2o } )
171 170 rexlimdvaa ( 𝐵 No → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) → 𝑧 ∈ { 1o , 2o } ) )
172 171 ad2antrl ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) → 𝑧 ∈ { 1o , 2o } ) )
173 172 adantr ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑧 ) → 𝑧 ∈ { 1o , 2o } ) )
174 157 173 sylbird ( ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) ∧ ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ) → ( 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) → 𝑧 ∈ { 1o , 2o } ) )
175 174 expimpd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ∧ 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) → 𝑧 ∈ { 1o , 2o } ) )
176 175 exlimdv ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( ∃ 𝑔 ( ∃ 𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ) ∧ 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) → 𝑧 ∈ { 1o , 2o } ) )
177 133 176 syl5bi ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( ∃ 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) → 𝑧 ∈ { 1o , 2o } ) )
178 177 abssdv ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → { 𝑧 ∣ ∃ 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } 𝑧 = ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) } ⊆ { 1o , 2o } )
179 123 178 eqsstrid ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ran ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ⊆ { 1o , 2o } )
180 elno2 ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ∈ No ↔ ( Fun ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ∧ dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ∈ On ∧ ran ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ⊆ { 1o , 2o } ) )
181 21 122 179 180 syl3anbrc ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ∈ No )
182 19 181 eqeltrd ( ( ¬ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 No 𝐵𝑉 ) ) → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) ∈ No )
183 17 182 pm2.61ian ( ( 𝐵 No 𝐵𝑉 ) → if ( ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 , ( ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( 𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) ∈ No )
184 1 183 eqeltrid ( ( 𝐵 No 𝐵𝑉 ) → 𝑇 No )