Metamath Proof Explorer

Theorem ax12el

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax12el ⊢¬∀xx=y→x=y→z∈w→∀xx=y→z∈w

Proof

Step Hyp Ref Expression
1 19.26 ⊢∀xx=z∧x=w↔∀xx=z∧∀xx=w
2 elequ1 ⊢x=y→x∈x↔y∈x
3 elequ2 ⊢x=y→y∈x↔y∈y
4 2 3 bitrd ⊢x=y→x∈x↔y∈y
5 4 adantl ⊢¬∀xx=y∧x=y→x∈x↔y∈y
6 ax-5 ⊢v∈v→∀xv∈v
7 ax-5 ⊢y∈y→∀vy∈y
8 elequ1 ⊢v=y→v∈v↔y∈v
9 elequ2 ⊢v=y→y∈v↔y∈y
10 8 9 bitrd ⊢v=y→v∈v↔y∈y
11 6 7 10 dvelimf-o ⊢¬∀xx=y→y∈y→∀xy∈y
12 4 biimprcd ⊢y∈y→x=y→x∈x
13 12 alimi ⊢∀xy∈y→∀xx=y→x∈x
14 11 13 syl6 ⊢¬∀xx=y→y∈y→∀xx=y→x∈x
15 14 adantr ⊢¬∀xx=y∧x=y→y∈y→∀xx=y→x∈x
16 5 15 sylbid ⊢¬∀xx=y∧x=y→x∈x→∀xx=y→x∈x
17 16 adantl ⊢∀xx=z∧x=w∧¬∀xx=y∧x=y→x∈x→∀xx=y→x∈x
18 elequ1 ⊢x=z→x∈x↔z∈x
19 elequ2 ⊢x=w→z∈x↔z∈w
20 18 19 sylan9bb ⊢x=z∧x=w→x∈x↔z∈w
21 20 sps-o ⊢∀xx=z∧x=w→x∈x↔z∈w
22 nfa1-o ⊢Ⅎx∀xx=z∧x=w
23 21 imbi2d ⊢∀xx=z∧x=w→x=y→x∈x↔x=y→z∈w
24 22 23 albid ⊢∀xx=z∧x=w→∀xx=y→x∈x↔∀xx=y→z∈w
25 21 24 imbi12d ⊢∀xx=z∧x=w→x∈x→∀xx=y→x∈x↔z∈w→∀xx=y→z∈w
26 25 adantr ⊢∀xx=z∧x=w∧¬∀xx=y∧x=y→x∈x→∀xx=y→x∈x↔z∈w→∀xx=y→z∈w
27 17 26 mpbid ⊢∀xx=z∧x=w∧¬∀xx=y∧x=y→z∈w→∀xx=y→z∈w
28 27 exp32 ⊢∀xx=z∧x=w→¬∀xx=y→x=y→z∈w→∀xx=y→z∈w
29 1 28 sylbir ⊢∀xx=z∧∀xx=w→¬∀xx=y→x=y→z∈w→∀xx=y→z∈w
30 elequ1 ⊢x=y→x∈w↔y∈w
31 30 ad2antll ⊢¬∀xx=w∧¬∀xx=y∧x=y→x∈w↔y∈w
32 ax-c14 ⊢¬∀xx=y→¬∀xx=w→y∈w→∀xy∈w
33 32 impcom ⊢¬∀xx=w∧¬∀xx=y→y∈w→∀xy∈w
34 33 adantrr ⊢¬∀xx=w∧¬∀xx=y∧x=y→y∈w→∀xy∈w
35 30 biimprcd ⊢y∈w→x=y→x∈w
36 35 alimi ⊢∀xy∈w→∀xx=y→x∈w
37 34 36 syl6 ⊢¬∀xx=w∧¬∀xx=y∧x=y→y∈w→∀xx=y→x∈w
38 31 37 sylbid ⊢¬∀xx=w∧¬∀xx=y∧x=y→x∈w→∀xx=y→x∈w
39 38 adantll ⊢∀xx=z∧¬∀xx=w∧¬∀xx=y∧x=y→x∈w→∀xx=y→x∈w
40 elequ1 ⊢x=z→x∈w↔z∈w
41 40 sps-o ⊢∀xx=z→x∈w↔z∈w
42 41 imbi2d ⊢∀xx=z→x=y→x∈w↔x=y→z∈w
43 42 dral2-o ⊢∀xx=z→∀xx=y→x∈w↔∀xx=y→z∈w
44 41 43 imbi12d ⊢∀xx=z→x∈w→∀xx=y→x∈w↔z∈w→∀xx=y→z∈w
45 44 ad2antrr ⊢∀xx=z∧¬∀xx=w∧¬∀xx=y∧x=y→x∈w→∀xx=y→x∈w↔z∈w→∀xx=y→z∈w
46 39 45 mpbid ⊢∀xx=z∧¬∀xx=w∧¬∀xx=y∧x=y→z∈w→∀xx=y→z∈w
47 46 exp32 ⊢∀xx=z∧¬∀xx=w→¬∀xx=y→x=y→z∈w→∀xx=y→z∈w
48 elequ2 ⊢x=y→z∈x↔z∈y
49 48 ad2antll ⊢¬∀xx=z∧¬∀xx=y∧x=y→z∈x↔z∈y
50 ax-c14 ⊢¬∀xx=z→¬∀xx=y→z∈y→∀xz∈y
51 50 imp ⊢¬∀xx=z∧¬∀xx=y→z∈y→∀xz∈y
52 51 adantrr ⊢¬∀xx=z∧¬∀xx=y∧x=y→z∈y→∀xz∈y
53 48 biimprcd ⊢z∈y→x=y→z∈x
54 53 alimi ⊢∀xz∈y→∀xx=y→z∈x
55 52 54 syl6 ⊢¬∀xx=z∧¬∀xx=y∧x=y→z∈y→∀xx=y→z∈x
56 49 55 sylbid ⊢¬∀xx=z∧¬∀xx=y∧x=y→z∈x→∀xx=y→z∈x
57 56 adantlr ⊢¬∀xx=z∧∀xx=w∧¬∀xx=y∧x=y→z∈x→∀xx=y→z∈x
58 19 sps-o ⊢∀xx=w→z∈x↔z∈w
59 58 imbi2d ⊢∀xx=w→x=y→z∈x↔x=y→z∈w
60 59 dral2-o ⊢∀xx=w→∀xx=y→z∈x↔∀xx=y→z∈w
61 58 60 imbi12d ⊢∀xx=w→z∈x→∀xx=y→z∈x↔z∈w→∀xx=y→z∈w
62 61 ad2antlr ⊢¬∀xx=z∧∀xx=w∧¬∀xx=y∧x=y→z∈x→∀xx=y→z∈x↔z∈w→∀xx=y→z∈w
63 57 62 mpbid ⊢¬∀xx=z∧∀xx=w∧¬∀xx=y∧x=y→z∈w→∀xx=y→z∈w
64 63 exp32 ⊢¬∀xx=z∧∀xx=w→¬∀xx=y→x=y→z∈w→∀xx=y→z∈w
65 ax6ev ⊢∃uu=w
66 ax6ev ⊢∃vv=z
67 ax-1 ⊢v∈u→x=y→v∈u
68 67 alrimiv ⊢v∈u→∀xx=y→v∈u
69 elequ1 ⊢v=z→v∈u↔z∈u
70 elequ2 ⊢u=w→z∈u↔z∈w
71 69 70 sylan9bb ⊢v=z∧u=w→v∈u↔z∈w
72 71 adantl ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→v∈u↔z∈w
73 dveeq2-o ⊢¬∀xx=z→v=z→∀xv=z
74 dveeq2-o ⊢¬∀xx=w→u=w→∀xu=w
75 73 74 im2anan9 ⊢¬∀xx=z∧¬∀xx=w→v=z∧u=w→∀xv=z∧∀xu=w
76 75 imp ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→∀xv=z∧∀xu=w
77 19.26 ⊢∀xv=z∧u=w↔∀xv=z∧∀xu=w
78 76 77 sylibr ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→∀xv=z∧u=w
79 nfa1-o ⊢Ⅎx∀xv=z∧u=w
80 71 sps-o ⊢∀xv=z∧u=w→v∈u↔z∈w
81 80 imbi2d ⊢∀xv=z∧u=w→x=y→v∈u↔x=y→z∈w
82 79 81 albid ⊢∀xv=z∧u=w→∀xx=y→v∈u↔∀xx=y→z∈w
83 78 82 syl ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→∀xx=y→v∈u↔∀xx=y→z∈w
84 72 83 imbi12d ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→v∈u→∀xx=y→v∈u↔z∈w→∀xx=y→z∈w
85 68 84 mpbii ⊢¬∀xx=z∧¬∀xx=w∧v=z∧u=w→z∈w→∀xx=y→z∈w
86 85 exp32 ⊢¬∀xx=z∧¬∀xx=w→v=z→u=w→z∈w→∀xx=y→z∈w
87 86 exlimdv ⊢¬∀xx=z∧¬∀xx=w→∃vv=z→u=w→z∈w→∀xx=y→z∈w
88 66 87 mpi ⊢¬∀xx=z∧¬∀xx=w→u=w→z∈w→∀xx=y→z∈w
89 88 exlimdv ⊢¬∀xx=z∧¬∀xx=w→∃uu=w→z∈w→∀xx=y→z∈w
90 65 89 mpi ⊢¬∀xx=z∧¬∀xx=w→z∈w→∀xx=y→z∈w
91 90 a1d ⊢¬∀xx=z∧¬∀xx=w→x=y→z∈w→∀xx=y→z∈w
92 91 a1d ⊢¬∀xx=z∧¬∀xx=w→¬∀xx=y→x=y→z∈w→∀xx=y→z∈w
93 29 47 64 92 4cases ⊢¬∀xx=y→x=y→z∈w→∀xx=y→z∈w