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 ⊢φ→∀x∈A∀y∈B∀z∈Cψ→w∈D∧v∈E→χ
iscnrm3lem2.2 ⊢φ→∀w∈D∀v∈Eχ→x∈A∧y∈B∧z∈C→ψ
Assertion iscnrm3lem2 ⊢φ→∀x∈A∀y∈B∀z∈Cψ↔∀w∈D∀v∈Eχ

Proof

Step Hyp Ref Expression
1 iscnrm3lem2.1 ⊢φ→∀x∈A∀y∈B∀z∈Cψ→w∈D∧v∈E→χ
2 iscnrm3lem2.2 ⊢φ→∀w∈D∀v∈Eχ→x∈A∧y∈B∧z∈C→ψ
3 2ax5 ⊢∀x∀y∀zx∈A∧y∈B∧z∈C→ψ→∀w∀v∀x∀y∀zx∈A∧y∈B∧z∈C→ψ
4 r3al ⊢∀x∈A∀y∈B∀z∈Cψ↔∀x∀y∀zx∈A∧y∈B∧z∈C→ψ
5 4 1 biimtrrid ⊢φ→∀x∀y∀zx∈A∧y∈B∧z∈C→ψ→w∈D∧v∈E→χ
6 5 2alimdv ⊢φ→∀w∀v∀x∀y∀zx∈A∧y∈B∧z∈C→ψ→∀w∀vw∈D∧v∈E→χ
7 3 6 syl5 ⊢φ→∀x∀y∀zx∈A∧y∈B∧z∈C→ψ→∀w∀vw∈D∧v∈E→χ
8 2ax5 ⊢∀w∀vw∈D∧v∈E→χ→∀y∀z∀w∀vw∈D∧v∈E→χ
9 8 alrimiv ⊢∀w∀vw∈D∧v∈E→χ→∀x∀y∀z∀w∀vw∈D∧v∈E→χ
10 r2al ⊢∀w∈D∀v∈Eχ↔∀w∀vw∈D∧v∈E→χ
11 10 2 biimtrrid ⊢φ→∀w∀vw∈D∧v∈E→χ→x∈A∧y∈B∧z∈C→ψ
12 11 2alimdv ⊢φ→∀y∀z∀w∀vw∈D∧v∈E→χ→∀y∀zx∈A∧y∈B∧z∈C→ψ
13 12 alimdv ⊢φ→∀x∀y∀z∀w∀vw∈D∧v∈E→χ→∀x∀y∀zx∈A∧y∈B∧z∈C→ψ
14 9 13 syl5 ⊢φ→∀w∀vw∈D∧v∈E→χ→∀x∀y∀zx∈A∧y∈B∧z∈C→ψ
15 7 14 impbid ⊢φ→∀x∀y∀zx∈A∧y∈B∧z∈C→ψ↔∀w∀vw∈D∧v∈E→χ
16 15 4 10 3bitr4g ⊢φ→∀x∈A∀y∈B∀z∈Cψ↔∀w∈D∀v∈Eχ