Metamath Proof Explorer

Theorem odfval

Description: Value of the order function. For a shorter proof using ax-rep , see odfvalALT . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) Remove depedency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

Ref Expression
Hypotheses odval.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odval.2 ⊢ · = ( .g ‘ 𝐺 )
odval.3 ⊢ 0 = ( 0g ‘ 𝐺 )
odval.4 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion odfval 𝑂 = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )

Proof

Step Hyp Ref Expression
1 odval.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odval.2 ⊢ · = ( .g ‘ 𝐺 )
3 odval.3 ⊢ 0 = ( 0g ‘ 𝐺 )
4 odval.4 ⊢ 𝑂 = ( od ‘ 𝐺 )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑋 )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( .g ‘ 𝑔 ) = ( .g ‘ 𝐺 ) )
8 7 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( .g ‘ 𝑔 ) = · )
9 8 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
11 10 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = 0 )
12 9 11 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ↔ ( 𝑦 · 𝑥 ) = 0 ) )
13 12 rabbidv ⊢ ( 𝑔 = 𝐺 → { 𝑦 ∈ ℕ ∣ ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } )
14 13 csbeq1d ⊢ ( 𝑔 = 𝐺 → ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
15 6 14 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
16 df-od ⊢ od = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
17 1 fvexi ⊢ 𝑋 ∈ V
18 nn0ex ⊢ ℕ0 ∈ V
19 nnex ⊢ ℕ ∈ V
20 19 rabex ⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ∈ V
21 eqeq1 ⊢ ( 𝑖 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } → ( 𝑖 = ∅ ↔ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ ) )
22 infeq1 ⊢ ( 𝑖 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } → inf ( 𝑖 , ℝ , < ) = inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) )
23 21 22 ifbieq2d ⊢ ( 𝑖 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } → if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) )
24 20 23 csbie ⊢ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) )
25 0nn0 ⊢ 0 ∈ ℕ0
26 25 a1i ⊢ ( ( ⊤ ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ ) → 0 ∈ ℕ0 )
27 df-ne ⊢ ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ ↔ ¬ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ )
28 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ⊆ ℕ
29 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
30 28 29 sseqtri ⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ⊆ ( ℤ≥ ‘ 1 )
31 infssuzcl ⊢ ( ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } )
32 30 31 mpan ⊢ ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } )
33 28 32 sseldi ⊢ ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ )
34 27 33 sylbir ⊢ ( ¬ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ )
35 34 nnnn0d ⊢ ( ¬ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ0 )
36 35 adantl ⊢ ( ( ⊤ ∧ ¬ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ0 )
37 26 36 ifclda ⊢ ( ⊤ → if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) ∈ ℕ0 )
38 37 mptru ⊢ if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) ∈ ℕ0
39 24 38 eqeltri ⊢ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ∈ ℕ0
40 39 rgenw ⊢ ∀ 𝑥 ∈ 𝑋 ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ∈ ℕ0
41 17 18 40 mptexw ⊢ ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) ∈ V
42 15 16 41 fvmpt ⊢ ( 𝐺 ∈ V → ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
43 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( od ‘ 𝐺 ) = ∅ )
44 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
45 1 44 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝑋 = ∅ )
46 45 mpteq1d ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ( 𝑥 ∈ ∅ ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
47 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ∅
48 46 47 eqtrdi ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ∅ )
49 43 48 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
50 42 49 pm2.61i ⊢ ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
51 4 50 eqtri ⊢ 𝑂 = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )