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 
|- ( ph -> ( A. x e. A A. y e. B A. z e. C ps -> ( ( w e. D /\ v e. E ) -> ch ) ) )
iscnrm3lem2.2 
|- ( ph -> ( A. w e. D A. v e. E ch -> ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
Assertion iscnrm3lem2 
|- ( ph -> ( A. x e. A A. y e. B A. z e. C ps <-> A. w e. D A. v e. E ch ) )

Proof

Step Hyp Ref Expression
1 iscnrm3lem2.1 
 |-  ( ph -> ( A. x e. A A. y e. B A. z e. C ps -> ( ( w e. D /\ v e. E ) -> ch ) ) )
2 iscnrm3lem2.2 
 |-  ( ph -> ( A. w e. D A. v e. E ch -> ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
3 2ax5 
 |-  ( A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) -> A. w A. v A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) )
4 r3al 
 |-  ( A. x e. A A. y e. B A. z e. C ps <-> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) )
5 4 1 syl5bir 
 |-  ( ph -> ( A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) -> ( ( w e. D /\ v e. E ) -> ch ) ) )
6 5 2alimdv 
 |-  ( ph -> ( A. w A. v A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) -> A. w A. v ( ( w e. D /\ v e. E ) -> ch ) ) )
7 3 6 syl5 
 |-  ( ph -> ( A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) -> A. w A. v ( ( w e. D /\ v e. E ) -> ch ) ) )
8 2ax5 
 |-  ( A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> A. y A. z A. w A. v ( ( w e. D /\ v e. E ) -> ch ) )
9 8 alrimiv 
 |-  ( A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> A. x A. y A. z A. w A. v ( ( w e. D /\ v e. E ) -> ch ) )
10 r2al 
 |-  ( A. w e. D A. v e. E ch <-> A. w A. v ( ( w e. D /\ v e. E ) -> ch ) )
11 10 2 syl5bir 
 |-  ( ph -> ( A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
12 11 2alimdv 
 |-  ( ph -> ( A. y A. z A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
13 12 alimdv 
 |-  ( ph -> ( A. x A. y A. z A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
14 9 13 syl5 
 |-  ( ph -> ( A. w A. v ( ( w e. D /\ v e. E ) -> ch ) -> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) ) )
15 7 14 impbid 
 |-  ( ph -> ( A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ps ) <-> A. w A. v ( ( w e. D /\ v e. E ) -> ch ) ) )
16 15 4 10 3bitr4g 
 |-  ( ph -> ( A. x e. A A. y e. B A. z e. C ps <-> A. w e. D A. v e. E ch ) )