Theorem pwsle 17670

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

Hypotheses

Ref	Expression
pwsle.y	⊢ 𝑌 = (𝑅 ↑s 𝐼)
pwsle.v	⊢ 𝐵 = (Base‘𝑌)
pwsle.o	⊢ 𝑂 = (le‘𝑅)
pwsle.l	⊢ ≤ = (le‘𝑌)

Assertion

Ref	Expression
pwsle	⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r 𝑂 ∩ (𝐵 × 𝐵)))

Proof of Theorem pwsle

Dummy variables 𝑓 𝑔 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3454	. . . . . . 7 ⊢ 𝑓 ∈ V
2		vex 3454	. . . . . . 7 ⊢ 𝑔 ∈ V
3	1, 2	prss 4775	. . . . . 6 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ 𝐵)
4		pwsle.v	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑌)
5		pwsle.y	. . . . . . . . . 10 ⊢ 𝑌 = (𝑅 ↑s 𝐼)
6		eqid 2760	. . . . . . . . . 10 ⊢ (Scalar‘𝑅) = (Scalar‘𝑅)
7	5, 6	pwsval 17663	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})))
8	7	fveq2d 6890	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑌) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))
9	4, 8	eqtrid 2807	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))
10	9	sseq2d 3940	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ({𝑓, 𝑔} ⊆ 𝐵 ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))))
11	3, 10	bitrid 286	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))))
12	11	anbi1d 643	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))))
13		fvconst2g 7209	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅)
14	13	ad4ant14 765	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅)
15	14	fveq2d 6890	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = (le‘𝑅))
16		pwsle.o	. . . . . . . . . 10 ⊢ 𝑂 = (le‘𝑅)
17	15, 16	eqtr4di 2813	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = 𝑂)
18	17	breqd 5113	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)𝑂(𝑔‘𝑥)))
19	18	ralbidva 3183	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥)))
20		eqid 2760	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
21		simpll 779	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑅 ∈ 𝑉)
22		simplr 781	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑊)
23		simprl 783	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵)
24	5, 20, 4, 21, 22, 23	pwselbas 17666	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓:𝐼⟶(Base‘𝑅))
25	24	ffnd 6711	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 Fn 𝐼)
26		simprr 785	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵)
27	5, 20, 4, 21, 22, 26	pwselbas 17666	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔:𝐼⟶(Base‘𝑅))
28	27	ffnd 6711	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 Fn 𝐼)
29		inidm 4123	. . . . . . . 8 ⊢ (𝐼 ∩ 𝐼) = 𝐼
30		eqidd 2761	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
31		eqidd 2761	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥))
32	25, 28, 23, 26, 29, 30, 31	ofrfvalg 7702	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓 ∘r 𝑂𝑔 ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥)))
33	19, 32	bitr4d 285	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ 𝑓 ∘r 𝑂𝑔))
34	33	pm5.32da 590	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘r 𝑂𝑔)))
35		brinxp2 5728	. . . . 5 ⊢ (𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔 ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘r 𝑂𝑔))
36	34, 35	bitr4di 292	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔))
37	12, 36	bitr3d 284	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔))
38	37	opabbidv 5170	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔})
39		pwsle.l	. . . 4 ⊢ ≤ = (le‘𝑌)
40	7	fveq2d 6890	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘𝑌) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))
41	39, 40	eqtrid 2807	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))
42		eqid 2760	. . . 4 ⊢ ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))
43		fvexd 6901	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V)
44		simpr 490	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊)
45		snex 5396	. . . . 5 ⊢ {𝑅} ∈ V
46		xpexg 7765	. . . . 5 ⊢ ((𝐼 ∈ 𝑊 ∧ {𝑅} ∈ V) → (𝐼 × {𝑅}) ∈ V)
47	44, 45, 46	sylancl 598	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) ∈ V)
48		eqid 2760	. . . 4 ⊢ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))
49		snnzg 4731	. . . . . 6 ⊢ (𝑅 ∈ 𝑉 → {𝑅} ≠ ∅)
50	49	adantr 486	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑅} ≠ ∅)
51		dmxp 5910	. . . . 5 ⊢ ({𝑅} ≠ ∅ → dom (𝐼 × {𝑅}) = 𝐼)
52	50, 51	syl 18	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → dom (𝐼 × {𝑅}) = 𝐼)
53		eqid 2760	. . . 4 ⊢ (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))
54	42, 43, 47, 48, 52, 53	prdsle 17639	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))})
55	41, 54	eqtrd 2795	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))})
56		relinxp 5791	. . . 4 ⊢ Rel ( ∘r 𝑂 ∩ (𝐵 × 𝐵))
57	56	a1i 11	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → Rel ( ∘r 𝑂 ∩ (𝐵 × 𝐵)))
58		dfrel4v 6181	. . 3 ⊢ (Rel ( ∘r 𝑂 ∩ (𝐵 × 𝐵)) ↔ ( ∘r 𝑂 ∩ (𝐵 × 𝐵)) = {⟨𝑓, 𝑔⟩ ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔})
59	57, 58	sylib 221	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ( ∘r 𝑂 ∩ (𝐵 × 𝐵)) = {⟨𝑓, 𝑔⟩ ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔})
60	38, 55, 59	3eqtr4d 2805	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r 𝑂 ∩ (𝐵 × 𝐵)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089  ∅c0 4278  {csn 4584  {cpr 4586   class class class wbr 5102  {copab 5166   × cxp 5648  dom cdm 5650  Rel wrel 5655  ‘cfv 6539  (class class class)co 7421   ∘_r cofr 7693  Basecbs 17393  Scalarcsca 17437  lecple 17441  X_scprds 17622   ↑_s cpws 17623

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-ofr 7695  df-om 7879  df-1st 8002  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-1o 8480  df-er 8721  df-map 8853  df-ixp 8930  df-en 8978  df-dom 8979  df-sdom 8980  df-fin 8981  df-sup 9438  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-2 12409  df-3 12410  df-4 12411  df-5 12412  df-6 12413  df-7 12414  df-8 12415  df-9 12416  df-n0 12611  df-z 12698  df-dec 12819  df-uz 12970  df-fz 13644  df-struct 17331  df-slot 17366  df-ndx 17378  df-base 17394  df-plusg 17447  df-mulr 17448  df-sca 17450  df-vsca 17451  df-ip 17452  df-tset 17453  df-ple 17454  df-ds 17456  df-hom 17458  df-cco 17459  df-prds 17624  df-pws 17626

This theorem is used by:  pwsleval  17671