Metamath Proof Explorer

Theorem noinfcbv

Description: Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 noinfcbv.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 breq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑦 <s 𝑥 ↔ 𝑦 <s 𝑎 ) )
3 2 notbid ⊢ ( 𝑥 = 𝑎 → ( ¬ 𝑦 <s 𝑥 ↔ ¬ 𝑦 <s 𝑎 ) )
4 3 ralbidv ⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑎 ) )
5 breq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 <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 𝑥 ) , 1o ⟩ = ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩
13 12 sneqi ⊢ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } = { ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩ }
14 10 13 uneq12i ⊢ ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) = ( ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩ } )
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 breq1 ⊢ ( 𝑢 = 𝑑 → ( 𝑢 <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 breq2 ⊢ ( 𝑣 = 𝑒 → ( 𝑑 <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 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = if ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 , ( ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩ } ) , ( 𝑐 ∈ { 𝑏 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑏 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑏 ) = ( 𝑒 ↾ suc 𝑏 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑑 ∈ 𝐵 ( 𝑐 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑐 ) = ( 𝑒 ↾ suc 𝑐 ) ) ∧ ( 𝑑 ‘ 𝑐 ) = 𝑎 ) ) ) )
78 1 77 eqtri ⊢ 𝑇 = if ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 , ( ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) ∪ { ⟨ dom ( ℩ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎 ) , 1o ⟩ } ) , ( 𝑐 ∈ { 𝑏 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑏 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑏 ) = ( 𝑒 ↾ suc 𝑏 ) ) ) } ↦ ( ℩ 𝑎 ∃ 𝑑 ∈ 𝐵 ( 𝑐 ∈ dom 𝑑 ∧ ∀ 𝑒 ∈ 𝐵 ( ¬ 𝑑 <s 𝑒 → ( 𝑑 ↾ suc 𝑐 ) = ( 𝑒 ↾ suc 𝑐 ) ) ∧ ( 𝑑 ‘ 𝑐 ) = 𝑎 ) ) ) )