Metamath Proof Explorer

Theorem nosupcbv

Description: Lemma to change bound variables in a surreal supremum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis nosupcbv.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion nosupcbv 𝑆 = if ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 , ( ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩ } ) , ( 𝑐 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 nosupcbv.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 <s 𝑦 ↔ 𝑎 <s 𝑦 ) )
3 2 notbid ⊢ ( 𝑥 = 𝑎 → ( ¬ 𝑥 <s 𝑦 ↔ ¬ 𝑎 <s 𝑦 ) )
4 3 ralbidv ⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑎 <s 𝑦 ) )
5 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 <s 𝑦 ↔ 𝑎 <s 𝑏 ) )
6 5 notbid ⊢ ( 𝑦 = 𝑏 → ( ¬ 𝑎 <s 𝑦 ↔ ¬ 𝑎 <s 𝑏 ) )
7 6 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑎 <s 𝑦 ↔ ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 )
8 4 7 bitrdi ⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) )
9 8 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 )
10 8 cbvriotavw ⊢ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) = ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 )
11 10 dmeqi ⊢ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) = dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 )
12 11 opeq1i ⊢ ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ = ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩
13 12 sneqi ⊢ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } = { ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩ }
14 10 13 uneq12i ⊢ ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) = ( ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩ } )
15 eleq1w ⊢ ( 𝑔 = 𝑐 → ( 𝑔 ∈ dom 𝑢 ↔ 𝑐 ∈ dom 𝑢 ) )
16 suceq ⊢ ( 𝑔 = 𝑐 → suc 𝑔 = suc 𝑐 )
17 16 reseq2d ⊢ ( 𝑔 = 𝑐 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑢 ↾ suc 𝑐 ) )
18 16 reseq2d ⊢ ( 𝑔 = 𝑐 → ( 𝑣 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑐 ) )
19 17 18 eqeq12d ⊢ ( 𝑔 = 𝑐 → ( ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ↔ ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) )
20 19 imbi2d ⊢ ( 𝑔 = 𝑐 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ) )
21 20 ralbidv ⊢ ( 𝑔 = 𝑐 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ) )
22 fveqeq2 ⊢ ( 𝑔 = 𝑐 → ( ( 𝑢 ‘ 𝑔 ) = 𝑥 ↔ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) )
23 15 21 22 3anbi123d ⊢ ( 𝑔 = 𝑐 → ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ↔ ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ) )
24 23 rexbidv ⊢ ( 𝑔 = 𝑐 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ) )
25 24 iotabidv ⊢ ( 𝑔 = 𝑐 → ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) = ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ) )
26 eqeq2 ⊢ ( 𝑥 = 𝑎 → ( ( 𝑢 ‘ 𝑐 ) = 𝑥 ↔ ( 𝑢 ‘ 𝑐 ) = 𝑎 ) )
27 26 3anbi3d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ↔ ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑎 ) ) )
28 27 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑎 ) ) )
29 dmeq ⊢ ( 𝑢 = 𝑒 → dom 𝑢 = dom 𝑒 )
30 29 eleq2d ⊢ ( 𝑢 = 𝑒 → ( 𝑐 ∈ dom 𝑢 ↔ 𝑐 ∈ dom 𝑒 ) )
31 breq2 ⊢ ( 𝑢 = 𝑒 → ( 𝑣 <s 𝑢 ↔ 𝑣 <s 𝑒 ) )
32 31 notbid ⊢ ( 𝑢 = 𝑒 → ( ¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑒 ) )
33 reseq1 ⊢ ( 𝑢 = 𝑒 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑒 ↾ suc 𝑐 ) )
34 33 eqeq1d ⊢ ( 𝑢 = 𝑒 → ( ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ↔ ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) )
35 32 34 imbi12d ⊢ ( 𝑢 = 𝑒 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ↔ ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ) )
36 35 ralbidv ⊢ ( 𝑢 = 𝑒 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ) )
37 breq1 ⊢ ( 𝑣 = 𝑓 → ( 𝑣 <s 𝑒 ↔ 𝑓 <s 𝑒 ) )
38 37 notbid ⊢ ( 𝑣 = 𝑓 → ( ¬ 𝑣 <s 𝑒 ↔ ¬ 𝑓 <s 𝑒 ) )
39 reseq1 ⊢ ( 𝑣 = 𝑓 → ( 𝑣 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) )
40 39 eqeq2d ⊢ ( 𝑣 = 𝑓 → ( ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ↔ ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) )
41 38 40 imbi12d ⊢ ( 𝑣 = 𝑓 → ( ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ↔ ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ) )
42 41 cbvralvw ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ↔ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) )
43 36 42 bitrdi ⊢ ( 𝑢 = 𝑒 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ↔ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ) )
44 fveq1 ⊢ ( 𝑢 = 𝑒 → ( 𝑢 ‘ 𝑐 ) = ( 𝑒 ‘ 𝑐 ) )
45 44 eqeq1d ⊢ ( 𝑢 = 𝑒 → ( ( 𝑢 ‘ 𝑐 ) = 𝑎 ↔ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) )
46 30 43 45 3anbi123d ⊢ ( 𝑢 = 𝑒 → ( ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑎 ) ↔ ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑎 ) ↔ ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) )
48 28 47 bitrdi ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ↔ ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
49 48 cbviotavw ⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑐 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑐 ) = ( 𝑣 ↾ suc 𝑐 ) ) ∧ ( 𝑢 ‘ 𝑐 ) = 𝑥 ) ) = ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) )
50 25 49 eqtrdi ⊢ ( 𝑔 = 𝑐 → ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) = ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
51 50 cbvmptv ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑐 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
52 eleq1w ⊢ ( 𝑦 = 𝑑 → ( 𝑦 ∈ dom 𝑢 ↔ 𝑑 ∈ dom 𝑢 ) )
53 suceq ⊢ ( 𝑦 = 𝑑 → suc 𝑦 = suc 𝑑 )
54 53 reseq2d ⊢ ( 𝑦 = 𝑑 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝑑 ) )
55 53 reseq2d ⊢ ( 𝑦 = 𝑑 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑑 ) )
56 54 55 eqeq12d ⊢ ( 𝑦 = 𝑑 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) )
57 56 imbi2d ⊢ ( 𝑦 = 𝑑 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) )
58 57 ralbidv ⊢ ( 𝑦 = 𝑑 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) )
59 52 58 anbi12d ⊢ ( 𝑦 = 𝑑 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝑑 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) ) )
60 59 rexbidv ⊢ ( 𝑦 = 𝑑 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑑 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) ) )
61 29 eleq2d ⊢ ( 𝑢 = 𝑒 → ( 𝑑 ∈ dom 𝑢 ↔ 𝑑 ∈ dom 𝑒 ) )
62 reseq1 ⊢ ( 𝑢 = 𝑒 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑒 ↾ suc 𝑑 ) )
63 62 eqeq1d ⊢ ( 𝑢 = 𝑒 → ( ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ↔ ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) )
64 32 63 imbi12d ⊢ ( 𝑢 = 𝑒 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ↔ ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) )
65 64 ralbidv ⊢ ( 𝑢 = 𝑒 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) )
66 reseq1 ⊢ ( 𝑣 = 𝑓 → ( 𝑣 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) )
67 66 eqeq2d ⊢ ( 𝑣 = 𝑓 → ( ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ↔ ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) )
68 38 67 imbi12d ⊢ ( 𝑣 = 𝑓 → ( ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ↔ ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) )
69 68 cbvralvw ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ↔ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) )
70 65 69 bitrdi ⊢ ( 𝑢 = 𝑒 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ↔ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) )
71 61 70 anbi12d ⊢ ( 𝑢 = 𝑒 → ( ( 𝑑 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) ↔ ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) ) )
72 71 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑑 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑑 ) = ( 𝑣 ↾ suc 𝑑 ) ) ) ↔ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) )
73 60 72 bitrdi ⊢ ( 𝑦 = 𝑑 → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) ) )
74 73 cbvabv ⊢ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } = { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) }
75 74 mpteq1i ⊢ ( 𝑐 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) ) = ( 𝑐 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
76 51 75 eqtri ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑐 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) )
77 9 14 76 ifbieq12i ⊢ if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = if ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 , ( ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩ } ) , ( 𝑐 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) ) )
78 1 77 eqtri ⊢ 𝑆 = if ( ∃ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 , ( ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏 ) , 2o ⟩ } ) , ( 𝑐 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ 𝐴 ( 𝑑 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑑 ) = ( 𝑓 ↾ suc 𝑑 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑒 ∈ 𝐴 ( 𝑐 ∈ dom 𝑒 ∧ ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑓 <s 𝑒 → ( 𝑒 ↾ suc 𝑐 ) = ( 𝑓 ↾ suc 𝑐 ) ) ∧ ( 𝑒 ‘ 𝑐 ) = 𝑎 ) ) ) )