Step Hyp Ref
Expression 1 porpss 6584 . . . 4
2 cnvpo 5550 . . . 4
3 1 , 2 mpbi 208 . . 3
4 pwfi 7835 . . . 4
5 4 biimpi 194 . . 3
6 frfi 7785 . . 3
7 3 , 5 , 6 sylancr 663 . 2
8 inss2 3718 . . . . . 6
9 pwexg 4636 . . . . . 6
10 ssexg 4598 . . . . . 6
11 8 , 9 , 10 sylancr 663 . . . . 5
12 0fin 7767 . . . . . . . 8
13 0elpw 4621 . . . . . . . 8
14 elin 3686 . . . . . . . 8
15 12 , 13 , 14 mpbir2an 920 . . . . . . 7
16 15 ne0ii 3791 . . . . . 6
17 fri 4846 . . . . . 6
18 8 , 16 , 17 mpanr12 685 . . . . 5
19 11 , 18 sylan 471 . . . 4
20 19 ex 434 . . 3
21 inss1 3717 . . . . . 6
22 simpl 457 . . . . . 6
23 21 , 22 sseldi 3501 . . . . 5
24 ralnex 2903 . . . . . . . 8
25 21 sseli 3499 . . . . . . . . . . . . . 14
26 25 adantr 465 . . . . . . . . . . . . 13
27 snfi 7616 . . . . . . . . . . . . 13
28 unfi 7807 . . . . . . . . . . . . 13
29 26 , 27 , 28 sylancl 662 . . . . . . . . . . . 12
30 elin 3686 . . . . . . . . . . . . . . . . 17
31 30 simprbi 464 . . . . . . . . . . . . . . . 16
32 31 elpwid 4022 . . . . . . . . . . . . . . 15
33 32 adantr 465 . . . . . . . . . . . . . 14
34 snssi 4174 . . . . . . . . . . . . . . 15
35 34 ad2antrl 727 . . . . . . . . . . . . . 14
36 33 , 35 unssd 3679 . . . . . . . . . . . . 13
37 vex 3112 . . . . . . . . . . . . . . 15
38 snex 4693 . . . . . . . . . . . . . . 15
39 37 , 38 unex 6598 . . . . . . . . . . . . . 14
40 39 elpw 4018 . . . . . . . . . . . . 13
41 36 , 40 sylibr 212 . . . . . . . . . . . 12
42 29 , 41 elind 3687 . . . . . . . . . . 11
43 disjsn 4090 . . . . . . . . . . . . . . 15
44 43 biimpri 206 . . . . . . . . . . . . . 14
45 vex 3112 . . . . . . . . . . . . . . 15
46 45 snnz 4148 . . . . . . . . . . . . . 14
47 disjpss 3877 . . . . . . . . . . . . . 14
48 44 , 46 , 47 sylancl 662 . . . . . . . . . . . . 13
49 48 ad2antll 728 . . . . . . . . . . . 12
50 39 , 37 brcnv 5190 . . . . . . . . . . . . 13
51 39 brrpss 6583 . . . . . . . . . . . . 13
52 50 , 51 bitri 249 . . . . . . . . . . . 12
53 49 , 52 sylibr 212 . . . . . . . . . . 11
54 breq1 4455 . . . . . . . . . . . 12
55 54 rspcev 3210 . . . . . . . . . . 11
56 42 , 53 , 55 syl2anc 661 . . . . . . . . . 10
57 56 expr 615 . . . . . . . . 9
58 57 con1d 124 . . . . . . . 8
59 24 , 58 syl5bi 217 . . . . . . 7
60 59 impancom 440 . . . . . 6
61 60 ssrdv 3509 . . . . 5
62 ssfi 7760 . . . . 5
63 23 , 61 , 62 syl2anc 661 . . . 4
64 63 rexlimiva 2945 . . 3
65 20 , 64 syl6 33 . 2
66 7 , 65 impbid2 204 1
