Metamath Proof Explorer


Theorem iscnrm3lem5

Description: Lemma for iscnrm3l . (Contributed by Zhi Wang, 3-Sep-2024)

Ref Expression
Hypotheses iscnrm3lem5.1 ( ( 𝑥 = 𝑆𝑦 = 𝑇 ) → ( 𝜑𝜓 ) )
iscnrm3lem5.2 ( ( 𝑥 = 𝑆𝑦 = 𝑇 ) → ( 𝜒𝜃 ) )
iscnrm3lem5.3 ( ( 𝜏𝜂𝜁 ) → ( 𝑆𝑉𝑇𝑊 ) )
iscnrm3lem5.4 ( ( 𝜏𝜂𝜁 ) → ( ( 𝜓𝜃 ) → 𝜎 ) )
Assertion iscnrm3lem5 ( 𝜏 → ( ∀ 𝑥𝑉𝑦𝑊 ( 𝜑𝜒 ) → ( 𝜂 → ( 𝜁𝜎 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscnrm3lem5.1 ( ( 𝑥 = 𝑆𝑦 = 𝑇 ) → ( 𝜑𝜓 ) )
2 iscnrm3lem5.2 ( ( 𝑥 = 𝑆𝑦 = 𝑇 ) → ( 𝜒𝜃 ) )
3 iscnrm3lem5.3 ( ( 𝜏𝜂𝜁 ) → ( 𝑆𝑉𝑇𝑊 ) )
4 iscnrm3lem5.4 ( ( 𝜏𝜂𝜁 ) → ( ( 𝜓𝜃 ) → 𝜎 ) )
5 1 2 imbi12d ( ( 𝑥 = 𝑆𝑦 = 𝑇 ) → ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜃 ) ) )
6 5 rspc2gv ( ( 𝑆𝑉𝑇𝑊 ) → ( ∀ 𝑥𝑉𝑦𝑊 ( 𝜑𝜒 ) → ( 𝜓𝜃 ) ) )
7 6 3 4 iscnrm3lem4 ( 𝜏 → ( ∀ 𝑥𝑉𝑦𝑊 ( 𝜑𝜒 ) → ( 𝜂 → ( 𝜁𝜎 ) ) ) )