Step | Hyp | Ref
| Expression |
1 | | bnj1408.3 |
. . . 4
|
2 | 1 | biimpri 218 |
. . 3
|
3 | | bnj1408.1 |
. . . . 5
|
4 | 3 | bnj1413 31103 |
. . . 4
|
5 | | simplll 798 |
. . . . . . . . 9
|
6 | | bnj213 30952 |
. . . . . . . . . . 11
|
7 | 6 | sseli 3599 |
. . . . . . . . . 10
|
8 | 7 | adantl 482 |
. . . . . . . . 9
|
9 | | bnj906 31000 |
. . . . . . . . 9
|
10 | 5, 8, 9 | syl2anc 693 |
. . . . . . . 8
|
11 | | bnj1318 31093 |
. . . . . . . . . . 11
|
12 | 11 | ssiun2s 4564 |
. . . . . . . . . 10
|
13 | | ssun4 3779 |
. . . . . . . . . . 11
|
14 | 13, 3 | syl6sseqr 3652 |
. . . . . . . . . 10
|
15 | 12, 14 | syl 17 |
. . . . . . . . 9
|
16 | 15 | adantl 482 |
. . . . . . . 8
|
17 | 10, 16 | sstrd 3613 |
. . . . . . 7
|
18 | | simpr 477 |
. . . . . . . . . . 11
|
19 | 18 | bnj1405 30907 |
. . . . . . . . . 10
|
20 | | biid 251 |
. . . . . . . . . 10
|
21 | | nfv 1843 |
. . . . . . . . . . . . 13
|
22 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
23 | | nfiu1 4550 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | nfun 3769 |
. . . . . . . . . . . . . . 15
|
25 | 3, 24 | nfcxfr 2762 |
. . . . . . . . . . . . . 14
|
26 | 25 | nfcri 2758 |
. . . . . . . . . . . . 13
|
27 | 21, 26 | nfan 1828 |
. . . . . . . . . . . 12
|
28 | 23 | nfcri 2758 |
. . . . . . . . . . . 12
|
29 | 27, 28 | nfan 1828 |
. . . . . . . . . . 11
|
30 | 29 | nf5ri 2065 |
. . . . . . . . . 10
|
31 | 19, 20, 30 | bnj1521 30921 |
. . . . . . . . 9
|
32 | | simplll 798 |
. . . . . . . . . . . . 13
|
33 | 32 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
34 | | bnj1147 31062 |
. . . . . . . . . . . . 13
|
35 | | simp3 1063 |
. . . . . . . . . . . . 13
|
36 | 34, 35 | bnj1213 30869 |
. . . . . . . . . . . 12
|
37 | 33, 36, 9 | syl2anc 693 |
. . . . . . . . . . 11
|
38 | | simp2 1062 |
. . . . . . . . . . . . 13
|
39 | 6, 38 | bnj1213 30869 |
. . . . . . . . . . . 12
|
40 | | bnj1125 31060 |
. . . . . . . . . . . 12
|
41 | 33, 39, 35, 40 | syl3anc 1326 |
. . . . . . . . . . 11
|
42 | 37, 41 | sstrd 3613 |
. . . . . . . . . 10
|
43 | | ssiun2 4563 |
. . . . . . . . . . . 12
|
44 | 43 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
45 | | ssun4 3779 |
. . . . . . . . . . . 12
|
46 | 45, 3 | syl6sseqr 3652 |
. . . . . . . . . . 11
|
47 | 44, 46 | syl 17 |
. . . . . . . . . 10
|
48 | 42, 47 | sstrd 3613 |
. . . . . . . . 9
|
49 | 31, 48 | bnj593 30815 |
. . . . . . . 8
|
50 | | nfcv 2764 |
. . . . . . . . . 10
|
51 | 50, 25 | nfss 3596 |
. . . . . . . . 9
|
52 | 51 | nf5ri 2065 |
. . . . . . . 8
|
53 | 49, 52 | bnj1397 30905 |
. . . . . . 7
|
54 | | simpr 477 |
. . . . . . . 8
|
55 | 3 | bnj1138 30859 |
. . . . . . . 8
|
56 | 54, 55 | sylib 208 |
. . . . . . 7
|
57 | 17, 53, 56 | mpjaodan 827 |
. . . . . 6
|
58 | 57 | ralrimiva 2966 |
. . . . 5
|
59 | | df-bnj19 30763 |
. . . . 5
|
60 | 58, 59 | sylibr 224 |
. . . 4
|
61 | 3 | bnj931 30841 |
. . . . 5
|
62 | 61 | a1i 11 |
. . . 4
|
63 | | bnj1408.4 |
. . . 4
|
64 | 4, 60, 62, 63 | syl3anbrc 1246 |
. . 3
|
65 | 1, 63 | bnj1124 31056 |
. . 3
|
66 | 2, 64, 65 | syl2anc 693 |
. 2
|
67 | | bnj906 31000 |
. . . . 5
|
68 | | iunss1 4532 |
. . . . 5
|
69 | | unss2 3784 |
. . . . 5
|
70 | 67, 68, 69 | 3syl 18 |
. . . 4
|
71 | | bnj1408.2 |
. . . 4
|
72 | 70, 3, 71 | 3sstr4g 3646 |
. . 3
|
73 | | biid 251 |
. . . 4
|
74 | | biid 251 |
. . . 4
|
75 | 71, 73, 74 | bnj1136 31065 |
. . 3
|
76 | 72, 75 | sseqtr4d 3642 |
. 2
|
77 | 66, 76 | eqssd 3620 |
1
|