Metamath Proof Explorer

Theorem sn-axrep5v

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

Ref Expression
Assertion sn-axrep5v ⊢∀w∈x∃*zφ→∃y∀zz∈y↔∃w∈xφ

Proof

Step Hyp Ref Expression
1 axrep6 ⊢∀w∃*zw∈x∧φ→∃y∀zz∈y↔∃w∈xw∈x∧φ
2 19.37v ⊢∃yw∈x→∀zφ→z=y↔w∈x→∃y∀zφ→z=y
3 impexp ⊢w∈x∧φ→z=y↔w∈x→φ→z=y
4 3 albii ⊢∀zw∈x∧φ→z=y↔∀zw∈x→φ→z=y
5 19.21v ⊢∀zw∈x→φ→z=y↔w∈x→∀zφ→z=y
6 4 5 bitri ⊢∀zw∈x∧φ→z=y↔w∈x→∀zφ→z=y
7 6 exbii ⊢∃y∀zw∈x∧φ→z=y↔∃yw∈x→∀zφ→z=y
8 df-mo ⊢∃*zφ↔∃y∀zφ→z=y
9 8 imbi2i ⊢w∈x→∃*zφ↔w∈x→∃y∀zφ→z=y
10 2 7 9 3bitr4i ⊢∃y∀zw∈x∧φ→z=y↔w∈x→∃*zφ
11 10 albii ⊢∀w∃y∀zw∈x∧φ→z=y↔∀ww∈x→∃*zφ
12 df-mo ⊢∃*zw∈x∧φ↔∃y∀zw∈x∧φ→z=y
13 12 albii ⊢∀w∃*zw∈x∧φ↔∀w∃y∀zw∈x∧φ→z=y
14 df-ral ⊢∀w∈x∃*zφ↔∀ww∈x→∃*zφ
15 11 13 14 3bitr4i ⊢∀w∃*zw∈x∧φ↔∀w∈x∃*zφ
16 rexanid ⊢∃w∈xw∈x∧φ↔∃w∈xφ
17 16 bibi2i ⊢z∈y↔∃w∈xw∈x∧φ↔z∈y↔∃w∈xφ
18 17 albii ⊢∀zz∈y↔∃w∈xw∈x∧φ↔∀zz∈y↔∃w∈xφ
19 18 exbii ⊢∃y∀zz∈y↔∃w∈xw∈x∧φ↔∃y∀zz∈y↔∃w∈xφ
20 1 15 19 3imtr3i ⊢∀w∈x∃*zφ→∃y∀zz∈y↔∃w∈xφ