Metamath Proof Explorer

Theorem odfvalALT

Description: Shorter proof of odfval using ax-rep . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses odval.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odval.2 ⊢ · = ( .g ‘ 𝐺 )
odval.3 ⊢ 0 = ( 0g ‘ 𝐺 )
odval.4 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion odfvalALT 𝑂 = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 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 15 16 1 mptfvmpt ⊢ ( 𝐺 ∈ V → ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
18 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( od ‘ 𝐺 ) = ∅ )
19 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
20 1 19 eqtrid ⊢ ( ¬ 𝐺 ∈ V → 𝑋 = ∅ )
21 20 mpteq1d ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ( 𝑥 ∈ ∅ ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
22 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ∅
23 21 22 eqtrdi ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) = ∅ )
24 18 23 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) )
25 17 24 pm2.61i ⊢ ( od ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
26 4 25 eqtri ⊢ 𝑂 = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )