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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 ( 𝜑 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧𝐷 ( ( 𝑥𝑧 ) < ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )