Step Hyp Ref
Expression
1 ssequn2 3676
. . . . . 6
2 pweq 4015
. . . . . . 7
3 eqimss 3555
. . . . . . 7
4 2 , 3 syl 16
. . . . . 6
5 1 , 4 sylbi 195
. . . . 5
6 ssequn1 3673
. . . . . 6
7 pweq 4015
. . . . . . 7
8 eqimss 3555
. . . . . . 7
9 7 , 8 syl 16
. . . . . 6
10 6 , 9 sylbi 195
. . . . 5
11 5 , 10 orim12i 516
. . . 4
12 11 orcoms 389
. . 3
13 ssun 3682
. . 3
14 12 , 13 syl 16
. 2
15 vex 3112
. . . . . . . . . . . . . . . . . . . 20
16 15 snss 4154
. . . . . . . . . . . . . . . . . . 19
17 vex 3112
. . . . . . . . . . . . . . . . . . . 20
18 17 snss 4154
. . . . . . . . . . . . . . . . . . 19
19 unss12 3675
. . . . . . . . . . . . . . . . . . 19
20 16 , 18 , 19 syl2anb 479
. . . . . . . . . . . . . . . . . 18
21 zfpair2 4692
. . . . . . . . . . . . . . . . . . . 20
22 21 elpw 4018
. . . . . . . . . . . . . . . . . . 19
23 df-pr 4032
. . . . . . . . . . . . . . . . . . . 20
24 23 sseq1i 3527
. . . . . . . . . . . . . . . . . . 19
25 22 , 24 bitr2i 250
. . . . . . . . . . . . . . . . . 18
26 20 , 25 sylib 196
. . . . . . . . . . . . . . . . 17
27 ssel 3497
. . . . . . . . . . . . . . . . 17
28 26 , 27 syl5 32
. . . . . . . . . . . . . . . 16
29 28 expcomd 438
. . . . . . . . . . . . . . 15
30 29 imp31 432
. . . . . . . . . . . . . 14
31 elun 3644
. . . . . . . . . . . . . 14
32 30 , 31 sylib 196
. . . . . . . . . . . . 13
33 21 elpw 4018
. . . . . . . . . . . . . . . 16
34 15 , 17 prss 4184
. . . . . . . . . . . . . . . 16
35 33 , 34 bitr4i 252
. . . . . . . . . . . . . . 15
36 35 simprbi 464
. . . . . . . . . . . . . 14
37 21 elpw 4018
. . . . . . . . . . . . . . . 16
38 15 , 17 prss 4184
. . . . . . . . . . . . . . . 16
39 37 , 38 bitr4i 252
. . . . . . . . . . . . . . 15
40 39 simplbi 460
. . . . . . . . . . . . . 14
41 36 , 40 orim12i 516
. . . . . . . . . . . . 13
42 32 , 41 syl 16
. . . . . . . . . . . 12
43 42 ord 377
. . . . . . . . . . 11
44 43 impancom 440
. . . . . . . . . 10
45 44 ssrdv 3509
. . . . . . . . 9
46 45 exp31 604
. . . . . . . 8
47 con1b 333
. . . . . . . 8
48 46 , 47 syl6ib 226
. . . . . . 7
49 48 com23 78
. . . . . 6
50 49 imp 429
. . . . 5
51 50 ssrdv 3509
. . . 4
52 51 ex 434
. . 3
53 52 orrd 378
. 2
54 14 , 53 impbii 188
1