Metamath Proof Explorer

Theorem opsrle

Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opsrle.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrle.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrle.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
opsrle.q ⊢ < = ( lt ‘ 𝑅 )
opsrle.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
opsrle.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
opsrle.l ⊢ ≤ = ( le ‘ 𝑂 )
opsrle.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsrle ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 opsrle.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 opsrle.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3 opsrle.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 opsrle.q ⊢ < = ( lt ‘ 𝑅 )
5 opsrle.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
6 opsrle.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7 opsrle.l ⊢ ≤ = ( le ‘ 𝑂 )
8 opsrle.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
9 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝐼 ∈ V )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑅 ∈ V )
12 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
13 1 2 3 4 5 6 9 10 11 12 opsrval ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
14 13 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( le ‘ 𝑂 ) = ( le ‘ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
15 1 ovexi ⊢ 𝑆 ∈ V
16 3 fvexi ⊢ 𝐵 ∈ V
17 16 16 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
18 vex ⊢ 𝑥 ∈ V
19 vex ⊢ 𝑦 ∈ V
20 18 19 prss ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
21 20 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) )
22 21 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
23 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⊆ ( 𝐵 × 𝐵 )
24 22 23 eqsstrri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⊆ ( 𝐵 × 𝐵 )
25 17 24 ssexi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ∈ V
26 pleid ⊢ le = Slot ( le ‘ ndx )
27 26 setsid ⊢ ( ( 𝑆 ∈ V ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ( le ‘ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
28 15 25 27 mp2an ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ( le ‘ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
29 14 7 28 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
30 reldmopsr ⊢ Rel dom ordPwSer
31 30 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 ordPwSer 𝑅 ) = ∅ )
32 31 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐼 ordPwSer 𝑅 ) = ∅ )
33 32 fveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) = ( ∅ ‘ 𝑇 ) )
34 2 33 syl5eq ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑂 = ( ∅ ‘ 𝑇 ) )
35 0fv ⊢ ( ∅ ‘ 𝑇 ) = ∅
36 34 35 eqtrdi ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑂 = ∅ )
37 36 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( le ‘ 𝑂 ) = ( le ‘ ∅ ) )
38 26 str0 ⊢ ∅ = ( le ‘ ∅ )
39 37 7 38 3eqtr4g ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ≤ = ∅ )
40 reldmpsr ⊢ Rel dom mPwSer
41 40 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
42 41 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
43 1 42 syl5eq ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑆 = ∅ )
44 43 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
45 base0 ⊢ ∅ = ( Base ‘ ∅ )
46 44 3 45 3eqtr4g ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝐵 = ∅ )
47 46 xpeq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐵 × 𝐵 ) = ( 𝐵 × ∅ ) )
48 xp0 ⊢ ( 𝐵 × ∅ ) = ∅
49 47 48 eqtrdi ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐵 × 𝐵 ) = ∅ )
50 sseq0 ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝐵 × 𝐵 ) = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ∅ )
51 24 49 50 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ∅ )
52 39 51 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
53 29 52 pm2.61dan ⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )