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 eqtrid ( ( 𝑅𝑉𝐼𝑊 ) → 𝐵 = ( 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 eqtrid ( ( 𝑅𝑉𝐼𝑊 ) → = ( 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 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )