Step | Hyp | Ref
| Expression |
1 | | zfregfr 4496 |
. 2
![A A](_ca.gif) |
2 | | epel 4222 |
. . . . . 6
![( (](lp.gif)
![b b](_b.gif) ![) )](rp.gif) |
3 | | epel 4222 |
. . . . . 6
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) |
4 | 2, 3 | anbi12i 456 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![c c](_c.gif) ![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![)
)](rp.gif) |
5 | | simpr 109 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![(
(](lp.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | | elirr 4464 |
. . . . . . . 8
![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) |
7 | | simprr 522 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![c c](_c.gif) ![) )](rp.gif) |
8 | | noel 3372 |
. . . . . . . . . . . . 13
![(/) (/)](varnothing.gif) |
9 | | eleq2 2204 |
. . . . . . . . . . . . 13
![( (](lp.gif)
![( (](lp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 8, 9 | mtbiri 665 |
. . . . . . . . . . . 12
![( (](lp.gif)
![b b](_b.gif) ![) )](rp.gif) |
11 | | simprl 521 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![b b](_b.gif) ![) )](rp.gif) |
12 | 10, 11 | nsyl3 616 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
13 | | elrabi 2841 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![{ {](lbrace.gif) ![{
{](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
14 | | reg3exmidlemwe.a |
. . . . . . . . . . . . . . . 16
![{ {](lbrace.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
15 | 13, 14 | eleq2s 2235 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
16 | | elpri 3555 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 15, 16 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 17 | orcomd 719 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 18 | 3ad2ant2 1004 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 19 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 12, 20 | ecased 1328 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
22 | | noel 3372 |
. . . . . . . . . . . . 13
![(/) (/)](varnothing.gif) |
23 | | eleq2 2204 |
. . . . . . . . . . . . 13
![( (](lp.gif)
![( (](lp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 22, 23 | mtbiri 665 |
. . . . . . . . . . . 12
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) |
25 | 24, 7 | nsyl3 616 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
26 | | elrabi 2841 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![{ {](lbrace.gif) ![{
{](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
27 | 26, 14 | eleq2s 2235 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
28 | | vex 2692 |
. . . . . . . . . . . . . . . 16
![_V
_V](rmcv.gif) |
29 | 28 | elpr 3553 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 27, 29 | sylib 121 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 30 | orcomd 719 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 31 | 3ad2ant3 1005 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 32 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 25, 33 | ecased 1328 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
35 | 7, 21, 34 | 3eltr3d 2223 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) ![) )](rp.gif) |
36 | 35 | ex 114 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![c c](_c.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 6, 36 | mtoi 654 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 37 | adantr 274 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 5, 38 | pm2.21dd 610 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![c c](_c.gif) ![) )](rp.gif) |
40 | 4, 39 | sylan2b 285 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![c c](_c.gif) ![) )](rp.gif) ![c c](_c.gif) ![) )](rp.gif) |
41 | 40 | ex 114 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![c c](_c.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 41 | rgen3 2522 |
. 2
![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif)
![c c](_c.gif) ![c c](_c.gif) ![) )](rp.gif) |
43 | | df-wetr 4264 |
. 2
![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif)
![c c](_c.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 1, 42, 43 | mpbir2an 927 |
1
![A A](_ca.gif) |