Metamath Proof Explorer

Theorem nosupdm

Description: The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypothesis nosupdm.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion nosupdm ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } )

Proof

Step Hyp Ref Expression
1 nosupdm.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 iffalse ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
3 1 2 eqtrid ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
4 3 dmeqd ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
5 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ∈ V
6 eqid ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
7 5 6 dmmpti ⊢ dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
8 4 7 eqtrdi ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
9 dmeq ⊢ ( 𝑢 = 𝑝 → dom 𝑢 = dom 𝑝 )
10 9 eleq2d ⊢ ( 𝑢 = 𝑝 → ( 𝑦 ∈ dom 𝑢 ↔ 𝑦 ∈ dom 𝑝 ) )
11 breq1 ⊢ ( 𝑣 = 𝑞 → ( 𝑣 <s 𝑢 ↔ 𝑞 <s 𝑢 ) )
12 11 notbid ⊢ ( 𝑣 = 𝑞 → ( ¬ 𝑣 <s 𝑢 ↔ ¬ 𝑞 <s 𝑢 ) )
13 reseq1 ⊢ ( 𝑣 = 𝑞 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) )
14 13 eqeq2d ⊢ ( 𝑣 = 𝑞 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) )
15 12 14 imbi12d ⊢ ( 𝑣 = 𝑞 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑞 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) )
16 15 cbvralvw ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) )
17 breq2 ⊢ ( 𝑢 = 𝑝 → ( 𝑞 <s 𝑢 ↔ 𝑞 <s 𝑝 ) )
18 17 notbid ⊢ ( 𝑢 = 𝑝 → ( ¬ 𝑞 <s 𝑢 ↔ ¬ 𝑞 <s 𝑝 ) )
19 reseq1 ⊢ ( 𝑢 = 𝑝 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑝 ↾ suc 𝑦 ) )
20 19 eqeq1d ⊢ ( 𝑢 = 𝑝 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ↔ ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) )
21 18 20 imbi12d ⊢ ( 𝑢 = 𝑝 → ( ( ¬ 𝑞 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) )
22 21 ralbidv ⊢ ( 𝑢 = 𝑝 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) )
23 16 22 bitrid ⊢ ( 𝑢 = 𝑝 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) )
24 10 23 anbi12d ⊢ ( 𝑢 = 𝑝 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝑦 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) ) )
25 24 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑦 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) )
26 eleq1w ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ dom 𝑝 ↔ 𝑧 ∈ dom 𝑝 ) )
27 suceq ⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 )
28 27 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑝 ↾ suc 𝑧 ) )
29 27 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑞 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑧 ) )
30 28 29 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ↔ ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) )
31 30 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) )
32 31 ralbidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ↔ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) )
33 26 32 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) ↔ ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ) )
34 33 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑝 ∈ 𝐴 ( 𝑦 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑦 ) = ( 𝑞 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ) )
35 25 34 bitrid ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) ) )
36 35 cbvabv ⊢ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } = { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) }
37 8 36 eqtrdi ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑧 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ dom 𝑝 ∧ ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 <s 𝑝 → ( 𝑝 ↾ suc 𝑧 ) = ( 𝑞 ↾ suc 𝑧 ) ) ) } )