Step | Hyp | Ref
| Expression |
1 | | elrabi 3359 |
. . . . 5
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | psgnfix.p |
. . . . . 6
|
4 | 2, 3 | symgbasf 17804 |
. . . . 5
|
5 | | ffn 6045 |
. . . . 5
|
6 | 1, 4, 5 | 3syl 18 |
. . . 4
|
7 | 6 | ad3antlr 767 |
. . 3
Word g
Word
..^
|
8 | | simpl 473 |
. . . . . . . 8
|
9 | 8 | adantr 481 |
. . . . . . 7
|
10 | 9 | adantr 481 |
. . . . . 6
Word g |
11 | | simp1 1061 |
. . . . . 6
Word
..^ Word |
12 | 10, 11 | anim12i 590 |
. . . . 5
Word g
Word
..^ Word |
13 | | psgnfix.z |
. . . . . 6
|
14 | 13 | eqcomi 2631 |
. . . . . . . 8
|
15 | 14 | fveq2i 6194 |
. . . . . . 7
|
16 | 3, 15 | eqtri 2644 |
. . . . . 6
|
17 | | psgnfix.r |
. . . . . 6
pmTrsp |
18 | 13, 16, 17 | gsmtrcl 17936 |
. . . . 5
Word g |
19 | 12, 18 | syl 17 |
. . . 4
Word g
Word
..^ g |
20 | 2, 3 | symgbasf 17804 |
. . . 4
g g |
21 | | ffn 6045 |
. . . 4
g g |
22 | 19, 20, 21 | 3syl 18 |
. . 3
Word g
Word
..^ g |
23 | 8 | ad3antrrr 766 |
. . . . . . . . . . . 12
Word g
Word
..^
|
24 | | simpr 477 |
. . . . . . . . . . . . 13
|
25 | 24 | ad3antrrr 766 |
. . . . . . . . . . . 12
Word g
Word
..^
|
26 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
27 | 17, 13, 26 | symgtrf 17889 |
. . . . . . . . . . . . . . 15
|
28 | | sswrd 13313 |
. . . . . . . . . . . . . . . 16
Word Word |
29 | 28 | sseld 3602 |
. . . . . . . . . . . . . . 15
Word
Word |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
Word Word |
31 | 30 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Word
..^ Word |
32 | 31 | adantl 482 |
. . . . . . . . . . . 12
Word g
Word
..^
Word |
33 | 23, 25, 32 | 3jca 1242 |
. . . . . . . . . . 11
Word g
Word
..^
Word |
34 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
35 | 34 | ralimi 2952 |
. . . . . . . . . . . . . 14
..^
..^ |
36 | 35 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
Word
..^ ..^ |
37 | 36 | adantl 482 |
. . . . . . . . . . . 12
Word g
Word
..^
..^ |
38 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
39 | 38 | eqcoms 2630 |
. . . . . . . . . . . . . . 15
..^ ..^ |
40 | 39 | raleqdv 3144 |
. . . . . . . . . . . . . 14
..^ ..^ |
41 | 40 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
Word
..^
..^ ..^ |
42 | 41 | adantl 482 |
. . . . . . . . . . . 12
Word g
Word
..^ ..^
..^ |
43 | 37, 42 | mpbird 247 |
. . . . . . . . . . 11
Word g
Word
..^
..^ |
44 | 13, 26 | gsmsymgrfix 17848 |
. . . . . . . . . . 11
Word
..^
g |
45 | 33, 43, 44 | sylc 65 |
. . . . . . . . . 10
Word g
Word
..^ g |
46 | 45 | eqcomd 2628 |
. . . . . . . . 9
Word g
Word
..^
g |
47 | 46 | adantr 481 |
. . . . . . . 8
Word
g Word
..^
g |
48 | | fveq2 6191 |
. . . . . . . . . 10
|
49 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
50 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
51 | 50 | elrab 3363 |
. . . . . . . . . . . 12
|
52 | 51 | simprbi 480 |
. . . . . . . . . . 11
|
53 | 52 | ad3antlr 767 |
. . . . . . . . . 10
Word g
Word
..^ |
54 | 48, 53 | sylan9eqr 2678 |
. . . . . . . . 9
Word
g Word
..^
|
55 | | fveq2 6191 |
. . . . . . . . . 10
g g |
56 | 55 | adantl 482 |
. . . . . . . . 9
Word
g Word
..^
g g |
57 | 54, 56 | eqeq12d 2637 |
. . . . . . . 8
Word
g Word
..^
g
g |
58 | 47, 57 | mpbird 247 |
. . . . . . 7
Word
g Word
..^
g |
59 | 58 | ex 450 |
. . . . . 6
Word g
Word
..^ g |
60 | 59 | adantr 481 |
. . . . 5
Word
g Word
..^
g |
61 | 60 | com12 32 |
. . . 4
Word g Word
..^
g |
62 | | fveq1 6190 |
. . . . . . . . 9
g g |
63 | 62 | adantl 482 |
. . . . . . . 8
Word
g
g |
64 | 63 | ad3antlr 767 |
. . . . . . 7
Word
g Word
..^
g |
65 | 64 | adantl 482 |
. . . . . 6
Word g
Word
..^
g |
66 | | simpr 477 |
. . . . . . . . . . . . 13
|
67 | | df-ne 2795 |
. . . . . . . . . . . . . 14
|
68 | 67 | biimpri 218 |
. . . . . . . . . . . . 13
|
69 | 66, 68 | anim12i 590 |
. . . . . . . . . . . 12
|
70 | | eldifsn 4317 |
. . . . . . . . . . . 12
|
71 | 69, 70 | sylibr 224 |
. . . . . . . . . . 11
|
72 | | fvres 6207 |
. . . . . . . . . . 11
|
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
|
74 | 73 | exp31 630 |
. . . . . . . . 9
|
75 | 74 | ad3antrrr 766 |
. . . . . . . 8
Word g
Word
..^
|
76 | 75 | imp 445 |
. . . . . . 7
Word
g Word
..^
|
77 | 76 | impcom 446 |
. . . . . 6
Word g
Word
..^
|
78 | 68 | anim2i 593 |
. . . . . . . . . . 11
|
79 | 78, 70 | sylibr 224 |
. . . . . . . . . 10
|
80 | 79 | ex 450 |
. . . . . . . . 9
|
81 | 80 | adantl 482 |
. . . . . . . 8
Word
g Word
..^
|
82 | 81 | impcom 446 |
. . . . . . 7
Word g
Word
..^
|
83 | | diffi 8192 |
. . . . . . . . . . . . 13
|
84 | 83 | ancri 575 |
. . . . . . . . . . . 12
|
85 | 84 | adantr 481 |
. . . . . . . . . . 11
|
86 | 85 | ad3antrrr 766 |
. . . . . . . . . 10
Word g
Word
..^
|
87 | | psgnfix.t |
. . . . . . . . . . . . . . 15
pmTrsp |
88 | | psgnfix.s |
. . . . . . . . . . . . . . 15
|
89 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
90 | 87, 88, 89 | symgtrf 17889 |
. . . . . . . . . . . . . 14
|
91 | | sswrd 13313 |
. . . . . . . . . . . . . . 15
Word Word |
92 | 91 | sseld 3602 |
. . . . . . . . . . . . . 14
Word
Word |
93 | 90, 92 | ax-mp 5 |
. . . . . . . . . . . . 13
Word Word |
94 | 93 | ad2antrl 764 |
. . . . . . . . . . . 12
Word g Word |
95 | 94 | adantr 481 |
. . . . . . . . . . 11
Word g
Word
..^
Word |
96 | | simpr2 1068 |
. . . . . . . . . . 11
Word g
Word
..^ |
97 | 95, 32, 96 | 3jca 1242 |
. . . . . . . . . 10
Word g
Word
..^ Word
Word
|
98 | 86, 97 | jca 554 |
. . . . . . . . 9
Word g
Word
..^
Word
Word
|
99 | 98 | ad2antrl 764 |
. . . . . . . 8
Word g
Word
..^
Word
Word
|
100 | | simpr 477 |
. . . . . . . . . . . 12
|
101 | 100 | ralimi 2952 |
. . . . . . . . . . 11
..^
..^
|
102 | 101 | 3ad2ant3 1084 |
. . . . . . . . . 10
Word
..^ ..^
|
103 | 102 | adantl 482 |
. . . . . . . . 9
Word g
Word
..^
..^ |
104 | 103 | ad2antrl 764 |
. . . . . . . 8
Word g
Word
..^
..^
|
105 | | incom 3805 |
. . . . . . . . . . 11
|
106 | | indif 3869 |
. . . . . . . . . . 11
|
107 | 105, 106 | eqtri 2644 |
. . . . . . . . . 10
|
108 | 107 | eqcomi 2631 |
. . . . . . . . 9
|
109 | 88, 89, 13, 26, 108 | gsmsymgreq 17852 |
. . . . . . . 8
Word
Word ..^
g g |
110 | 99, 104, 109 | sylc 65 |
. . . . . . 7
Word g
Word
..^
g g |
111 | | fveq2 6191 |
. . . . . . . . 9
g g |
112 | | fveq2 6191 |
. . . . . . . . 9
g g |
113 | 111, 112 | eqeq12d 2637 |
. . . . . . . 8
g g
g g |
114 | 113 | rspcva 3307 |
. . . . . . 7
g g g g |
115 | 82, 110, 114 | syl2anc 693 |
. . . . . 6
Word g
Word
..^
g g |
116 | 65, 77, 115 | 3eqtr3d 2664 |
. . . . 5
Word g
Word
..^
g |
117 | 116 | ex 450 |
. . . 4
Word g
Word
..^
g |
118 | 61, 117 | pm2.61i 176 |
. . 3
Word
g Word
..^
g |
119 | 7, 22, 118 | eqfnfvd 6314 |
. 2
Word g
Word
..^
g |
120 | 119 | exp31 630 |
1
Word g
Word
..^ g |