prdsleval

Description: Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
	prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	prdsleval.l	⊢ ≤ = ( le ‘ 𝑌 )
Assertion	prdsleval	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
2		prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6		prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		prdsleval.l	⊢ ≤ = ( le ‘ 𝑌 )
9		df-br	⊢ ( 𝐹 ≤ 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ≤ )
10		fnex	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
11	5 4 10	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ V )
12	5	fndmd	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
13	1 3 11 2 12 8	prdsle	⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
14		vex	⊢ 𝑓 ∈ V
15		vex	⊢ 𝑔 ∈ V
16	14 15	prss	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 )
17	16	anbi1i	⊢ ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
18	17	opabbii	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) }
19	13 18	eqtr4di	⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
20	19	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ≤ ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) )
21	9 20	bitrid	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) )
22		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
23		fveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
24	22 23	breqan12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
25	24	ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
26	25	opelopab2a	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
27	6 7 26	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
28	21 27	bitrd	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem prdsleval

Proof