Metamath Proof Explorer


Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

Ref Expression
Hypotheses joinval2.b 𝐵 = ( Base ‘ 𝐾 )
joinval2.l = ( le ‘ 𝐾 )
joinval2.j = ( join ‘ 𝐾 )
joinval2.k ( 𝜑𝐾𝑉 )
joinval2.x ( 𝜑𝑋𝐵 )
joinval2.y ( 𝜑𝑌𝐵 )
Assertion joinval2lem ( ( 𝑋𝐵𝑌𝐵 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑧𝑥 𝑧 ) ) ↔ ( ( 𝑋 𝑥𝑌 𝑥 ) ∧ ∀ 𝑧𝐵 ( ( 𝑋 𝑧𝑌 𝑧 ) → 𝑥 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 joinval2.b 𝐵 = ( Base ‘ 𝐾 )
2 joinval2.l = ( le ‘ 𝐾 )
3 joinval2.j = ( join ‘ 𝐾 )
4 joinval2.k ( 𝜑𝐾𝑉 )
5 joinval2.x ( 𝜑𝑋𝐵 )
6 joinval2.y ( 𝜑𝑌𝐵 )
7 breq1 ( 𝑦 = 𝑋 → ( 𝑦 𝑥𝑋 𝑥 ) )
8 breq1 ( 𝑦 = 𝑌 → ( 𝑦 𝑥𝑌 𝑥 ) )
9 7 8 ralprg ( ( 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑥 ↔ ( 𝑋 𝑥𝑌 𝑥 ) ) )
10 breq1 ( 𝑦 = 𝑋 → ( 𝑦 𝑧𝑋 𝑧 ) )
11 breq1 ( 𝑦 = 𝑌 → ( 𝑦 𝑧𝑌 𝑧 ) )
12 10 11 ralprg ( ( 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑧 ↔ ( 𝑋 𝑧𝑌 𝑧 ) ) )
13 12 imbi1d ( ( 𝑋𝐵𝑌𝐵 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑧𝑥 𝑧 ) ↔ ( ( 𝑋 𝑧𝑌 𝑧 ) → 𝑥 𝑧 ) ) )
14 13 ralbidv ( ( 𝑋𝐵𝑌𝐵 ) → ( ∀ 𝑧𝐵 ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑧𝑥 𝑧 ) ↔ ∀ 𝑧𝐵 ( ( 𝑋 𝑧𝑌 𝑧 ) → 𝑥 𝑧 ) ) )
15 9 14 anbi12d ( ( 𝑋𝐵𝑌𝐵 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } 𝑦 𝑧𝑥 𝑧 ) ) ↔ ( ( 𝑋 𝑥𝑌 𝑥 ) ∧ ∀ 𝑧𝐵 ( ( 𝑋 𝑧𝑌 𝑧 ) → 𝑥 𝑧 ) ) ) )