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	biimtrrid	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) )
6	5	2alimdv	⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) )
7	3 6	syl5	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) → ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) )
8		2ax5	⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) )
9	8	alrimiv	⊢ ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) )
10		r2al	⊢ ( ∀ 𝑤 ∈ 𝐷 ∀ 𝑣 ∈ 𝐸 𝜒 ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) )
11	10 2	biimtrrid	⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) )
12	11	2alimdv	⊢ ( 𝜑 → ( ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) )
13	12	alimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) )
14	9 13	syl5	⊢ ( 𝜑 → ( ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ) )
15	7 14	impbid	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) ↔ ∀ 𝑤 ∀ 𝑣 ( ( 𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸 ) → 𝜒 ) ) )
16	15 4 10	3bitr4g	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ↔ ∀ 𝑤 ∈ 𝐷 ∀ 𝑣 ∈ 𝐸 𝜒 ) )