HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem axrepndlem2 3739
Description: Lemma for the Axiom of Replacement with no distinct variable conditions.
Assertion
Ref Expression
axrepndlem2 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
Proof of Theorem axrepndlem2
StepHypRef Expression
1 eq6 826 . . . . 5 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
2 eq6 826 . . . . 5 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
31, 2hban 704 . . . 4 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ∧ ¬ ∀x x = z))
4 eq6 826 . . . . . . 7 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
5 eq6 826 . . . . . . 7 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
64, 5hban 704 . . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀y(¬ ∀x x = y ∧ ¬ ∀x x = z))
7 eq6 826 . . . . . . . 8 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
8 eq6 826 . . . . . . . 8 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
97, 8hban 704 . . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ∧ ¬ ∀x x = z))
10 ax-17 925 . . . . . . . . . 10 ⊢ (φ → ∀wφ)
1110hbsb3 875 . . . . . . . . 9 ⊢ ([w / x]φ → ∀x[w / x]φ)
1211a1i 7 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ([w / x]φ → ∀x[w / x]φ))
13 ax-12 802 . . . . . . . . . 10 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
1413com12 13 . . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (z = y → ∀x z = y)))
1514imp 277 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (z = y → ∀x z = y))
163, 12, 15hbimd 787 . . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (([w / x]φ → z = y) → ∀x([w / x]φ → z = y)))
179, 16hbald 790 . . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀z([w / x]φ → z = y) → ∀x∀z([w / x]φ → z = y)))
186, 17hbexd 791 . . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃y∀z([w / x]φ → z = y) → ∀x∃y∀z([w / x]φ → z = y)))
19 ddeel1 1003 . . . . . . . 8 ⊢ (¬ ∀x x = z → (z ∈ w → ∀x z ∈ w))
2019adantl 305 . . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (z ∈ w → ∀x z ∈ w))
21 ax-17 925 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ∧ ¬ ∀x x = z))
22 ddeel2 1004 . . . . . . . . . 10 ⊢ (¬ ∀x x = y → (w ∈ y → ∀x w ∈ y))
2322adantr 306 . . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w ∈ y → ∀x w ∈ y))
246, 12hbald 790 . . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀y[w / x]φ → ∀x∀y[w / x]φ))
2523, 24hband 788 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((w ∈ y ∧ ∀y[w / x]φ) → ∀x(w ∈ y ∧ ∀y[w / x]φ)))
2621, 25hbexd 791 . . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w(w ∈ y ∧ ∀y[w / x]φ) → ∀x∃w(w ∈ y ∧ ∀y[w / x]φ)))
273, 20, 26hbbid 789 . . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) → ∀x(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))))
289, 27hbald 790 . . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) → ∀x∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))))
293, 18, 28hbimd 787 . . . 4 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))) → ∀x(∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)))))
30 nd5 3736 . . . . . . . . 9 ⊢ (¬ ∀x x = y → (w = x → ∀y w = x))
3130adantr 306 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ∀y w = x))
3231imdistani 340 . . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
33 hba1 698 . . . . . . . . 9 ⊢ (∀y w = x → ∀y∀y w = x)
346, 33hban 704 . . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → ∀y((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
35 nd5 3736 . . . . . . . . . . 11 ⊢ (¬ ∀x x = z → (w = x → ∀z w = x))
3635imdistani 340 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ w = x) → (¬ ∀x x = z ∧ ∀z w = x))
37 hba1 698 . . . . . . . . . . . 12 ⊢ (∀z w = x → ∀z∀z w = x)
388, 37hban 704 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ∀z w = x) → ∀z(¬ ∀x x = z ∧ ∀z w = x))
39 sbequ12r 866 . . . . . . . . . . . . . 14 ⊢ (w = x → ([w / x]φ ↔ φ))
4039imbi1d 465 . . . . . . . . . . . . 13 ⊢ (w = x → (([w / x]φ → z = y) ↔ (φ → z = y)))
4140a4s 682 . . . . . . . . . . . 12 ⊢ (∀z w = x → (([w / x]φ → z = y) ↔ (φ → z = y)))
4241adantl 305 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ∀z w = x) → (([w / x]φ → z = y) ↔ (φ → z = y)))
4338, 42biald 782 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ ∀z w = x) → (∀z([w / x]φ → z = y) ↔ ∀z(φ → z = y)))
4436, 43syl 12 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ w = x) → (∀z([w / x]φ → z = y) ↔ ∀z(φ → z = y)))
45 pm3.27 260 . . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ¬ ∀x x = z)
46 ax-4 673 . . . . . . . . 9 ⊢ (∀y w = x → w = x)
4744, 45, 46syl2an 349 . . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (∀z([w / x]φ → z = y) ↔ ∀z(φ → z = y)))
4834, 47biexd 783 . . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (∃y∀z([w / x]φ → z = y) ↔ ∃y∀z(φ → z = y)))
4932, 48syl 12 . . . . . 6 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∃y∀z([w / x]φ → z = y) ↔ ∃y∀z(φ → z = y)))
5035adantl 305 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ∀z w = x))
5150imdistani 340 . . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀z w = x))
529, 37hban 704 . . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀z w = x) → ∀z((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀z w = x))
53 a14b 820 . . . . . . . . . . 11 ⊢ (w = x → (z ∈ w ↔ z ∈ x))
5453adantl 305 . . . . . . . . . 10 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (z ∈ w ↔ z ∈ x))
55 a13b 819 . . . . . . . . . . . . . . 15 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
5655adantl 305 . . . . . . . . . . . . . 14 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (w ∈ y ↔ x ∈ y))
57 sbal2 1005 . . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∀y y = x → ([w / x]∀yφ ↔ ∀y[w / x]φ))
5857eq4ds 823 . . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀x x = y → ([w / x]∀yφ ↔ ∀y[w / x]φ))
5958bicomd 399 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = y → (∀y[w / x]φ ↔ [w / x]∀yφ))
60 sbequ12r 866 . . . . . . . . . . . . . . . 16 ⊢ (w = x → ([w / x]∀yφ ↔ ∀yφ))
6159, 60sylan9bb 418 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ∧ w = x) → (∀y[w / x]φ ↔ ∀yφ))
6261adantlr 310 . . . . . . . . . . . . . 14 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∀y[w / x]φ ↔ ∀yφ))
6356, 62anbi12d 476 . . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((w ∈ y ∧ ∀y[w / x]φ) ↔ (x ∈ y ∧ ∀yφ)))
6463exp 291 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ((w ∈ y ∧ ∀y[w / x]φ) ↔ (x ∈ y ∧ ∀yφ))))
653, 25, 64cbvexd 978 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w(w ∈ y ∧ ∀y[w / x]φ) ↔ ∃x(x ∈ y ∧ ∀yφ)))
6665adantr 306 . . . . . . . . . 10 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∃w(w ∈ y ∧ ∀y[w / x]φ) ↔ ∃x(x ∈ y ∧ ∀yφ)))
6754, 66bibi12d 477 . . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) ↔ (z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
68 ax-4 673 . . . . . . . . 9 ⊢ (∀z w = x → w = x)
6967, 68sylan2 346 . . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀z w = x) → ((z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) ↔ (z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
7052, 69biald 782 . . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀z w = x) → (∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
7151, 70syl 12 . . . . . 6 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ)) ↔ ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
7249, 71imbi12d 474 . . . . 5 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))) ↔ (∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)))))
7372exp 291 . . . 4 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ((∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))) ↔ (∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))))
743, 29, 73cbvexd 978 . . 3 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w(∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))) ↔ ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)))))
75 axrepndlem1 3738 . . 3 ⊢ (¬ ∀y y = z → ∃w(∃y∀z([w / x]φ → z = y) → ∀z(z ∈ w ↔ ∃w(w ∈ y ∧ ∀y[w / x]φ))))
7674, 75syl5bi 183 . 2 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (¬ ∀y y = z → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ)))))
7776imp 277 1 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ¬ ∀y y = z) → ∃x(∃y∀z(φ → z = y) → ∀z(z ∈ x ↔ ∃x(x ∈ y ∧ ∀yφ))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  [wsb 852
This theorem is referenced by:  axrepnd 3740
This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075
This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349
metamath.org