Metamath Proof Explorer


Theorem pwsleval

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 ‘ 𝑌 )
pwsleval.r ( 𝜑𝑅𝑉 )
pwsleval.i ( 𝜑𝐼𝑊 )
pwsleval.a ( 𝜑𝐹𝐵 )
pwsleval.b ( 𝜑𝐺𝐵 )
Assertion pwsleval ( 𝜑 → ( 𝐹 𝐺 ↔ ∀ 𝑥𝐼 ( 𝐹𝑥 ) 𝑂 ( 𝐺𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 pwsle.y 𝑌 = ( 𝑅s 𝐼 )
2 pwsle.v 𝐵 = ( Base ‘ 𝑌 )
3 pwsle.o 𝑂 = ( le ‘ 𝑅 )
4 pwsle.l = ( le ‘ 𝑌 )
5 pwsleval.r ( 𝜑𝑅𝑉 )
6 pwsleval.i ( 𝜑𝐼𝑊 )
7 pwsleval.a ( 𝜑𝐹𝐵 )
8 pwsleval.b ( 𝜑𝐺𝐵 )
9 1 2 3 4 pwsle ( ( 𝑅𝑉𝐼𝑊 ) → = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )
10 5 6 9 syl2anc ( 𝜑 = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )
11 10 breqd ( 𝜑 → ( 𝐹 𝐺𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
12 brinxp ( ( 𝐹𝐵𝐺𝐵 ) → ( 𝐹r 𝑂 𝐺𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
13 7 8 12 syl2anc ( 𝜑 → ( 𝐹r 𝑂 𝐺𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
14 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 1 14 2 5 6 7 pwselbas ( 𝜑𝐹 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
16 15 ffnd ( 𝜑𝐹 Fn 𝐼 )
17 1 14 2 5 6 8 pwselbas ( 𝜑𝐺 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
18 17 ffnd ( 𝜑𝐺 Fn 𝐼 )
19 inidm ( 𝐼𝐼 ) = 𝐼
20 eqidd ( ( 𝜑𝑥𝐼 ) → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) )
21 eqidd ( ( 𝜑𝑥𝐼 ) → ( 𝐺𝑥 ) = ( 𝐺𝑥 ) )
22 16 18 7 8 19 20 21 ofrfvalg ( 𝜑 → ( 𝐹r 𝑂 𝐺 ↔ ∀ 𝑥𝐼 ( 𝐹𝑥 ) 𝑂 ( 𝐺𝑥 ) ) )
23 11 13 22 3bitr2d ( 𝜑 → ( 𝐹 𝐺 ↔ ∀ 𝑥𝐼 ( 𝐹𝑥 ) 𝑂 ( 𝐺𝑥 ) ) )