Metamath Proof Explorer

Theorem ax12eq

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

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