Metamath Proof Explorer

Theorem pwsle

Description: Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015)

Ref Expression
Hypotheses pwsle.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsle.v ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsle.o ⊢ 𝑂 = ( le ‘ 𝑅 )
pwsle.l ⊢ ≤ = ( le ‘ 𝑌 )
Assertion pwsle ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 pwsle.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsle.v ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsle.o ⊢ 𝑂 = ( le ‘ 𝑅 )
4 pwsle.l ⊢ ≤ = ( le ‘ 𝑌 )
5 vex ⊢ 𝑓 ∈ V
6 vex ⊢ 𝑔 ∈ V
7 5 6 prss ⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 )
8 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
9 1 8 pwsval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
10 9 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
11 2 10 syl5eq ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
12 11 sseq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( { 𝑓 , 𝑔 } ⊆ 𝐵 ↔ { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) )
13 7 12 syl5bb ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) )
14 13 anbi1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
15 fvconst2g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
16 15 ad4ant14 ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
17 16 fveq2d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( le ‘ 𝑅 ) )
18 17 3 eqtr4di ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = 𝑂 )
19 18 breqd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) )
20 19 ralbidva ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) )
21 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
22 simpll ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑅 ∈ 𝑉 )
23 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑊 )
24 simprl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
25 1 21 2 22 23 24 pwselbas ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
26 25 ffnd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 Fn 𝐼 )
27 simprr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
28 1 21 2 22 23 27 pwselbas ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
29 28 ffnd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 Fn 𝐼 )
30 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
31 eqidd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
32 eqidd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
33 26 29 24 27 30 31 32 ofrfvalg ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ∘r 𝑂 𝑔 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) )
34 20 33 bitr4d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ 𝑓 ∘r 𝑂 𝑔 ) )
35 34 pm5.32da ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑓 ∘r 𝑂 𝑔 ) ) )
36 brinxp2 ⊢ ( 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ↔ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑓 ∘r 𝑂 𝑔 ) )
37 35 36 bitr4di ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ) )
38 14 37 bitr3d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ) )
39 38 opabbidv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } )
40 9 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( le ‘ 𝑌 ) = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
41 4 40 syl5eq ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
42 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
43 fvexd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑅 ) ∈ V )
44 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 )
45 snex ⊢ { 𝑅 } ∈ V
46 xpexg ⊢ ( ( 𝐼 ∈ 𝑊 ∧ { 𝑅 } ∈ V ) → ( 𝐼 × { 𝑅 } ) ∈ V )
47 44 45 46 sylancl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑅 } ) ∈ V )
48 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
49 snnzg ⊢ ( 𝑅 ∈ 𝑉 → { 𝑅 } ≠ ∅ )
50 49 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑅 } ≠ ∅ )
51 dmxp ⊢ ( { 𝑅 } ≠ ∅ → dom ( 𝐼 × { 𝑅 } ) = 𝐼 )
52 50 51 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → dom ( 𝐼 × { 𝑅 } ) = 𝐼 )
53 eqid ⊢ ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
54 42 43 47 48 52 53 prdsle ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
55 41 54 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
56 relinxp ⊢ Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) )
57 56 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )
58 dfrel4v ⊢ ( Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) ↔ ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } )
59 57 58 sylib ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } )
60 39 55 59 3eqtr4d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )