Metamath Proof Explorer

Theorem noinfdm

Description: Next, we calculate the domain of T . This is mostly to change bound variables. (Contributed by Scott Fenton, 8-Aug-2024)

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

Proof

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