Step | Hyp | Ref
| Expression |
1 | | simp2 956 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC Spac
![`](backtick.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | spacval 6282 |
. . . . 5
![(](lp.gif) NC Spac ![`](backtick.gif) ![M](_cm.gif)
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 2 | 3ad2ant1 976 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC Spac ![`](backtick.gif) ![M](_cm.gif)
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 3 | eleqtrd 2429 |
. . 3
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | spacssnc 6284 |
. . . . . 6
![(](lp.gif) NC Spac ![`](backtick.gif) ![M](_cm.gif)
NC ![)](rp.gif) |
6 | 5 | sselda 3273 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![)](rp.gif) NC ![)](rp.gif) |
7 | 6 | 3adant3 975 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC NC ![)](rp.gif) |
8 | | simp3 957 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC ![(](lp.gif) ↑c
0c
NC ![)](rp.gif) |
9 | | 2nnc 6167 |
. . . . . 6
2c
Nn |
10 | | ceclnn1 6189 |
. . . . . 6
![(](lp.gif) 2c Nn NC ![(](lp.gif)
↑c 0c NC 2c ↑c ![N](_cn.gif)
NC ![)](rp.gif) |
11 | 9, 10 | mp3an1 1264 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC 2c
↑c ![N](_cn.gif) NC ![)](rp.gif) |
12 | 7, 8, 11 | syl2anc 642 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC 2c ↑c ![N](_cn.gif)
NC ![)](rp.gif) |
13 | | eqidd 2354 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | ovex 5551 |
. . . . . 6
2c
↑c ![N](_cn.gif) ![_V](rmcv.gif) |
15 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
NC
NC ![)](rp.gif) ![)](rp.gif) |
16 | | oveq2 5531 |
. . . . . . . . 9
![(](lp.gif) 2c
↑c ![x](_x.gif) 2c ↑c
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
2c
↑c ![x](_x.gif) 2c ↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 15, 17 | 3anbi13d 1254 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![(](lp.gif) NC NC 2c ↑c
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) NC 2c
↑c ![N](_cn.gif) NC ![)](rp.gif) ![)](rp.gif) |
20 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) 2c ↑c ![N](_cn.gif) 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 19, 20 | 3anbi23d 1255 |
. . . . . . 7
![(](lp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) ![(](lp.gif) NC NC 2c ↑c
![N](_cn.gif) ![)](rp.gif) ![(](lp.gif) NC 2c ↑c ![N](_cn.gif)
NC 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | eqid 2353 |
. . . . . . 7
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
23 | 18, 21, 22 | brabg 4706 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Spac ![`](backtick.gif) ![M](_cm.gif) 2c
↑c ![N](_cn.gif) ![_V](rmcv.gif) ![(](lp.gif) ![N](_cn.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) NC 2c ↑c ![N](_cn.gif)
NC 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 14, 23 | mpan2 652 |
. . . . 5
![(](lp.gif) Spac ![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif) ![N](_cn.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) NC 2c ↑c ![N](_cn.gif)
NC 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | 3ad2ant2 977 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC ![(](lp.gif) ![N](_cn.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) 2c ↑c ![N](_cn.gif) ![(](lp.gif) NC 2c ↑c ![N](_cn.gif)
NC 2c ↑c ![N](_cn.gif)
2c
↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 7, 12, 13, 25 | mpbir3and 1135 |
. . 3
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC ![N](_cn.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) 2c ↑c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | eqid 2353 |
. . . 4
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif)
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
28 | 27 | clos1conn 5879 |
. . 3
![(](lp.gif) ![(](lp.gif) Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![N](_cn.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC
2c
↑c ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) 2c ↑c ![N](_cn.gif) ![)](rp.gif) 2c
↑c ![N](_cn.gif)
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC 2c ↑c
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 4, 26, 28 | syl2anc 642 |
. 2
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC 2c ↑c ![N](_cn.gif)
Clos1 ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) NC NC
2c
↑c ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 29, 3 | eleqtrrd 2430 |
1
![(](lp.gif) ![(](lp.gif) NC Spac
![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif)
↑c 0c NC 2c ↑c ![N](_cn.gif)
Spac ![`](backtick.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |