Metamath Proof Explorer


Theorem iscnrm3lem2

Description: Lemma for iscnrm3 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024)

Ref Expression
Hypotheses iscnrm3lem2.1 ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶 𝜓 → ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
iscnrm3lem2.2 ( 𝜑 → ( ∀ 𝑤𝐷𝑣𝐸 𝜒 → ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
Assertion iscnrm3lem2 ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶 𝜓 ↔ ∀ 𝑤𝐷𝑣𝐸 𝜒 ) )

Proof

Step Hyp Ref Expression
1 iscnrm3lem2.1 ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶 𝜓 → ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
2 iscnrm3lem2.2 ( 𝜑 → ( ∀ 𝑤𝐷𝑣𝐸 𝜒 → ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
3 2ax5 ( ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) → ∀ 𝑤𝑣𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) )
4 r3al ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶 𝜓 ↔ ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) )
5 4 1 syl5bir ( 𝜑 → ( ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) → ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
6 5 2alimdv ( 𝜑 → ( ∀ 𝑤𝑣𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) → ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
7 3 6 syl5 ( 𝜑 → ( ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) → ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
8 2ax5 ( ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ∀ 𝑦𝑧𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) )
9 8 alrimiv ( ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ∀ 𝑥𝑦𝑧𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) )
10 r2al ( ∀ 𝑤𝐷𝑣𝐸 𝜒 ↔ ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) )
11 10 2 syl5bir ( 𝜑 → ( ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
12 11 2alimdv ( 𝜑 → ( ∀ 𝑦𝑧𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ∀ 𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
13 12 alimdv ( 𝜑 → ( ∀ 𝑥𝑦𝑧𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
14 9 13 syl5 ( 𝜑 → ( ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) → ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ) )
15 7 14 impbid ( 𝜑 → ( ∀ 𝑥𝑦𝑧 ( ( 𝑥𝐴𝑦𝐵𝑧𝐶 ) → 𝜓 ) ↔ ∀ 𝑤𝑣 ( ( 𝑤𝐷𝑣𝐸 ) → 𝜒 ) ) )
16 15 4 10 3bitr4g ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶 𝜓 ↔ ∀ 𝑤𝐷𝑣𝐸 𝜒 ) )