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

Metamath Proof Explorer

Theorem axrepndlem1

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axrepndlem1 ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 axrep2 ⊢ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑤 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) )
2 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
3 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
4 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑧
5 nfs1v ⊢ Ⅎ 𝑧 [ 𝑤 / 𝑧 ] 𝜑
6 5 a1i ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 [ 𝑤 / 𝑧 ] 𝜑 )
7 nfcvd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑤 )
8 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑦 )
9 7 8 nfeqd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑤 = 𝑦 )
10 6 9 nfimd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) )
11 sbequ12r ⊢ ( 𝑤 = 𝑧 → ( [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 ) )
12 equequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 = 𝑦 ↔ 𝑧 = 𝑦 ) )
13 11 12 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) ) )
14 13 a1i ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑧 → ( ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) ) ) )
15 4 10 14 cbvald ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑤 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
16 3 15 exbid ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑦 ∀ 𝑤 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
17 nfvd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑤 ∈ 𝑥 )
18 8 nfcrd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑥 ∈ 𝑦 )
19 3 6 nfald ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 )
20 18 19 nfand ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) )
21 2 20 nfexd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) )
22 17 21 nfbid ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) )
23 elequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
24 23 adantl ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( 𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
25 nfeqf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑤 = 𝑧 )
26 3 25 nfan1 ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 )
27 11 adantl ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( [ 𝑤 / 𝑧 ] 𝜑 ↔ 𝜑 ) )
28 26 27 albid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ↔ ∀ 𝑦 𝜑 ) )
29 28 anbi2d ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
30 29 exbidv ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
31 24 30 bibi12d ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧 ) → ( ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
32 31 ex ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
33 4 22 32 cbvald ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
34 16 33 imbi12d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ( ∃ 𝑦 ∀ 𝑤 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
35 2 34 exbid ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑤 ( [ 𝑤 / 𝑧 ] 𝜑 → 𝑤 = 𝑦 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑧 ] 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
36 1 35 mpbii ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )