This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralxp3f

Description: Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses ralxp3f.1 ⊢ Ⅎ 𝑦 𝜑
ralxp3f.2 ⊢ Ⅎ 𝑧 𝜑
ralxp3f.3 ⊢ Ⅎ 𝑤 𝜑
ralxp3f.4 ⊢ Ⅎ 𝑥 𝜓
ralxp3f.5 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion ralxp3f ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )

Proof

Step Hyp Ref Expression
1 ralxp3f.1 ⊢ Ⅎ 𝑦 𝜑
2 ralxp3f.2 ⊢ Ⅎ 𝑧 𝜑
3 ralxp3f.3 ⊢ Ⅎ 𝑤 𝜑
4 ralxp3f.4 ⊢ Ⅎ 𝑥 𝜓
5 ralxp3f.5 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → ( 𝜑 ↔ 𝜓 ) )
6 df-ral ⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) )
7 el2xptp ⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ )
8 7 imbi1i ⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
9 3 r19.23 ⊢ ( ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
10 9 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
11 2 r19.23 ⊢ ( ∀ 𝑧 ∈ 𝐵 ( ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
12 10 11 bitri ⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
13 12 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
14 1 r19.23 ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
15 13 14 bitr2i ⊢ ( ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
16 8 15 bitri ⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
17 16 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
18 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
19 ralcom4 ⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
20 ralcom4 ⊢ ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) )
21 otex ⊢ ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ ∈ V
22 4 21 5 ceqsal ⊢ ( ∀ 𝑥 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ 𝜓 )
23 22 ralbii ⊢ ( ∀ 𝑤 ∈ 𝐶 ∀ 𝑥 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑤 ∈ 𝐶 𝜓 )
24 20 23 bitr3i ⊢ ( ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑤 ∈ 𝐶 𝜓 )
25 24 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑥 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
26 19 25 bitr3i ⊢ ( ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
27 26 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
28 18 27 bitr3i ⊢ ( ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 ( 𝑥 = ⟨ 𝑦 , 𝑧 , 𝑤 ⟩ → 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )
29 6 17 28 3bitri ⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐶 𝜓 )