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		df-mo	⊢ ( ∃* 𝑧 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) ↔ ∃ 𝑦 ∀ 𝑧 ( if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) → 𝑧 = 𝑦 ) )
22	20 21	mpbir	⊢ ∃* 𝑧 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 )
23	1 22	mpg	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 if- ( 𝜑 , 𝑧 = 𝑎 , 𝑧 = 𝑏 ) )