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

Metamath Proof Explorer

Theorem sn-axrep5v

Description: A condensed form of axrep5 . (Contributed by SN, 21-Sep-2023)

Ref Expression
Assertion sn-axrep5v ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )

Proof

Step Hyp Ref Expression
1 axrep6 ⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) )
2 19.37v ⊢ ( ∃ 𝑦 ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
3 impexp ⊢ ( ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) )
4 3 albii ⊢ ( ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) )
5 19.21v ⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝜑 → 𝑧 = 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
6 4 5 bitri ⊢ ( ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
7 6 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
8 dfmo ⊢ ( ∃* 𝑧 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) )
9 8 imbi2i ⊢ ( ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ↔ ( 𝑤 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
10 2 7 9 3bitr4i ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
11 10 albii ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
12 dfmo ⊢ ( ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) )
13 12 albii ⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) → 𝑧 = 𝑦 ) )
14 df-ral ⊢ ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
15 11 13 14 3bitr4i ⊢ ( ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 )
16 rexanid ⊢ ( ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑤 ∈ 𝑥 𝜑 )
17 16 bibi2i ⊢ ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
18 17 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
19 18 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )
20 1 15 19 3imtr3i ⊢ ( ∀ 𝑤 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 𝜑 ) )