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 ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ( ∃ 𝑦𝑧 ( 𝜑𝑧 = 𝑦 ) → ∀ 𝑧 ( 𝑧𝑥 ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ∀ 𝑦 𝜑 ) ) ) )