Metamath Proof Explorer

Theorem ax12indalem

Description: Lemma for ax12inda2 and ax12inda . (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12indalem.1 
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Assertion ax12indalem 
|- ( -. A. y y = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax12indalem.1 
 |-  ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
2 ax-1 
 |-  ( A. x ph -> ( x = y -> A. x ph ) )
3 2 axc4i-o 
 |-  ( A. x ph -> A. x ( x = y -> A. x ph ) )
4 3 a1i 
 |-  ( A. z z = x -> ( A. x ph -> A. x ( x = y -> A. x ph ) ) )
5 biidd 
 |-  ( A. z z = x -> ( ph <-> ph ) )
6 5 dral1-o 
 |-  ( A. z z = x -> ( A. z ph <-> A. x ph ) )
7 6 imbi2d 
 |-  ( A. z z = x -> ( ( x = y -> A. z ph ) <-> ( x = y -> A. x ph ) ) )
8 7 dral2-o 
 |-  ( A. z z = x -> ( A. x ( x = y -> A. z ph ) <-> A. x ( x = y -> A. x ph ) ) )
9 4 6 8 3imtr4d 
 |-  ( A. z z = x -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
10 9 aecoms-o 
 |-  ( A. x x = z -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
11 10 a1d 
 |-  ( A. x x = z -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
12 11 a1d 
 |-  ( A. x x = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
13 12 adantr 
 |-  ( ( A. x x = z /\ -. A. y y = z ) -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
14 simplr 
 |-  ( ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ -. A. x x = y ) /\ x = y ) -> -. A. x x = y )
15 aecom-o 
 |-  ( A. z z = x -> A. x x = z )
16 15 con3i 
 |-  ( -. A. x x = z -> -. A. z z = x )
17 aecom-o 
 |-  ( A. z z = y -> A. y y = z )
18 17 con3i 
 |-  ( -. A. y y = z -> -. A. z z = y )
19 axc9 
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
20 19 imp 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> A. z x = y ) )
21 16 18 20 syl2an 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( x = y -> A. z x = y ) )
22 21 imp 
 |-  ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ x = y ) -> A. z x = y )
23 22 adantlr 
 |-  ( ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ -. A. x x = y ) /\ x = y ) -> A. z x = y )
24 hbnae-o 
 |-  ( -. A. x x = y -> A. z -. A. x x = y )
25 hba1-o 
 |-  ( A. z x = y -> A. z A. z x = y )
26 24 25 hban 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> A. z ( -. A. x x = y /\ A. z x = y ) )
27 ax-c5 
 |-  ( A. z x = y -> x = y )
28 1 imp 
 |-  ( ( -. A. x x = y /\ x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
29 27 28 sylan2 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
30 26 29 alimdh 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
31 14 23 30 syl2anc 
 |-  ( ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
32 ax-11 
 |-  ( A. z A. x ( x = y -> ph ) -> A. x A. z ( x = y -> ph ) )
33 hbnae-o 
 |-  ( -. A. x x = z -> A. x -. A. x x = z )
34 hbnae-o 
 |-  ( -. A. y y = z -> A. x -. A. y y = z )
35 33 34 hban 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> A. x ( -. A. x x = z /\ -. A. y y = z ) )
36 hbnae-o 
 |-  ( -. A. x x = z -> A. z -. A. x x = z )
37 hbnae-o 
 |-  ( -. A. y y = z -> A. z -. A. y y = z )
38 36 37 hban 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> A. z ( -. A. x x = z /\ -. A. y y = z ) )
39 38 21 nf5dh 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> F/ z x = y )
40 19.21t 
 |-  ( F/ z x = y -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
41 39 40 syl 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
42 35 41 albidh 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( A. x A. z ( x = y -> ph ) <-> A. x ( x = y -> A. z ph ) ) )
43 32 42 imbitrid 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
44 43 ad2antrr 
 |-  ( ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ -. A. x x = y ) /\ x = y ) -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
45 31 44 syld 
 |-  ( ( ( ( -. A. x x = z /\ -. A. y y = z ) /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
46 45 exp31 
 |-  ( ( -. A. x x = z /\ -. A. y y = z ) -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
47 13 46 pm2.61ian 
 |-  ( -. A. y y = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )