Metamath Proof Explorer

Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023)

Ref Expression
Assertion axprlem3 ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑧 if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 )
2 1 axrep4 ⊢ ( ∀ 𝑠 ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
3 ax6evr ⊢ ∃ 𝑧 𝑥 = 𝑧
4 ifptru ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑥 ) )
5 4 biimpd ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑥 ) )
6 equtrr ⊢ ( 𝑥 = 𝑧 → ( 𝑤 = 𝑥 → 𝑤 = 𝑧 ) )
7 5 6 sylan9r ⊢ ( ( 𝑥 = 𝑧 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
8 7 alrimiv ⊢ ( ( 𝑥 = 𝑧 ∧ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
9 8 expcom ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( 𝑥 = 𝑧 → ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) ) )
10 9 eximdv ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( ∃ 𝑧 𝑥 = 𝑧 → ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) ) )
11 3 10 mpi ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
12 ax6evr ⊢ ∃ 𝑧 𝑦 = 𝑧
13 ifpfal ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑦 ) )
14 13 biimpd ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑦 ) )
15 14 adantl ⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑦 ) )
16 simpl ⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → 𝑦 = 𝑧 )
17 equtr ⊢ ( 𝑤 = 𝑦 → ( 𝑦 = 𝑧 → 𝑤 = 𝑧 ) )
18 15 16 17 syl6ci ⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
19 18 alrimiv ⊢ ( ( 𝑦 = 𝑧 ∧ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) → ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
20 19 expcom ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( 𝑦 = 𝑧 → ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) ) )
21 20 eximdv ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( ∃ 𝑧 𝑦 = 𝑧 → ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) ) )
22 12 21 mpi ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 ) )
23 11 22 pm2.61i ⊢ ∃ 𝑧 ∀ 𝑤 ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) → 𝑤 = 𝑧 )
24 2 23 mpg ⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )