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

Metamath Proof Explorer

Theorem axrepndlem2

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) (Proof shortened by Mario Carneiro, 6-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axrepndlem1 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑤 ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
2 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
3 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
4 2 3 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
5 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑧
7 5 6 nfan ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
8 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
9 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧
10 8 9 nfan ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
11 nfs1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
12 11 a1i ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑 )
13 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑧 )
14 13 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 )
15 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
16 15 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 )
17 14 16 nfeqd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 = 𝑦 )
18 12 17 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) )
19 10 18 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) )
20 7 19 nfexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) )
21 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 )
22 14 21 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 ∈ 𝑤 )
23 nfv ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
24 21 16 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 ∈ 𝑦 )
25 7 12 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 )
26 24 25 nfand ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) )
27 23 26 nfexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) )
28 22 27 nfbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) )
29 10 28 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) )
30 20 29 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ) )
31 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑤 )
32 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
33 32 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑥 )
34 31 33 nfeqd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑤 = 𝑥 )
35 7 34 nfan1 ⊢ Ⅎ 𝑦 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 )
36 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑤 )
37 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑥 )
38 37 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑥 )
39 36 38 nfeqd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑧 𝑤 = 𝑥 )
40 10 39 nfan1 ⊢ Ⅎ 𝑧 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 )
41 sbequ12r ⊢ ( 𝑤 = 𝑥 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
42 41 imbi1d ⊢ ( 𝑤 = 𝑥 → ( ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) ) )
43 42 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) ↔ ( 𝜑 → 𝑧 = 𝑦 ) ) )
44 40 43 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
45 35 44 exbid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) ) )
46 elequ2 ⊢ ( 𝑤 = 𝑥 → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥 ) )
47 46 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥 ) )
48 elequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
49 48 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
50 41 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
51 35 50 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 𝜑 ) )
52 49 51 anbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
53 52 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
54 4 26 53 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
55 54 adantr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) )
56 47 55 bibi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
57 40 56 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )
58 45 57 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
59 58 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) ) )
60 4 30 59 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( ∃ 𝑦 ∀ 𝑧 ( [ 𝑤 / 𝑥 ] 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ ∀ 𝑦 [ 𝑤 / 𝑥 ] 𝜑 ) ) ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
61 1 60 imbitrid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
62 61 imp ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ∃ 𝑥 ( ∃ 𝑦 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )