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

Metamath Proof Explorer

Theorem sn-axprlem3

Description: axprlem3 using only Tarski's FOL axiom schemes and ax-rep . (Contributed by SN, 22-Sep-2023)

Ref Expression
Assertion sn-axprlem3 ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) )

Proof

Step Hyp Ref Expression
1 axrep6 ⊢ ( ∀ 𝑤 ∃* 𝑧 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) ) )
2 ax6evr ⊢ ∃ 𝑦 𝑎 = 𝑦
3 ifptru ⊢ ( 𝜑 → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) ↔ 𝑧 = 𝑎 ) )
4 3 biimpd ⊢ ( 𝜑 → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑎 ) )
5 equtrr ⊢ ( 𝑎 = 𝑦 → ( 𝑧 = 𝑎 → 𝑧 = 𝑦 ) )
6 4 5 sylan9r ⊢ ( ( 𝑎 = 𝑦 ∧ 𝜑 ) → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
7 6 alrimiv ⊢ ( ( 𝑎 = 𝑦 ∧ 𝜑 ) → ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
8 7 expcom ⊢ ( 𝜑 → ( 𝑎 = 𝑦 → ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) ) )
9 8 eximdv ⊢ ( 𝜑 → ( ∃ 𝑦 𝑎 = 𝑦 → ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) ) )
10 2 9 mpi ⊢ ( 𝜑 → ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
11 ax6evr ⊢ ∃ 𝑦 𝑏 = 𝑦
12 ifpfal ⊢ ( ¬ 𝜑 → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) ↔ 𝑧 = 𝑏 ) )
13 12 biimpd ⊢ ( ¬ 𝜑 → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑏 ) )
14 equtrr ⊢ ( 𝑏 = 𝑦 → ( 𝑧 = 𝑏 → 𝑧 = 𝑦 ) )
15 13 14 sylan9r ⊢ ( ( 𝑏 = 𝑦 ∧ ¬ 𝜑 ) → ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
16 15 alrimiv ⊢ ( ( 𝑏 = 𝑦 ∧ ¬ 𝜑 ) → ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
17 16 expcom ⊢ ( ¬ 𝜑 → ( 𝑏 = 𝑦 → ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) ) )
18 17 eximdv ⊢ ( ¬ 𝜑 → ( ∃ 𝑦 𝑏 = 𝑦 → ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) ) )
19 11 18 mpi ⊢ ( ¬ 𝜑 → ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
20 10 19 pm2.61i ⊢ ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 )
21 dfmo ⊢ ( ∃* 𝑧 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) ↔ ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
22 20 21 mpbir ⊢ ∃* 𝑧 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 )
23 1 22 mpg ⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) )