Proof of Theorem konigthlem
Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . . . . . . 9
|
2 | | fvex 6201 |
. . . . . . . . . . 11
|
3 | | eqid 2622 |
. . . . . . . . . . 11
|
4 | 2, 3 | fnmpti 6022 |
. . . . . . . . . 10
|
5 | 1 | mptex 6486 |
. . . . . . . . . . . 12
|
6 | | konigth.4 |
. . . . . . . . . . . . 13
|
7 | 6 | fvmpt2 6291 |
. . . . . . . . . . . 12
|
8 | 5, 7 | mpan2 707 |
. . . . . . . . . . 11
|
9 | 8 | fneq1d 5981 |
. . . . . . . . . 10
|
10 | 4, 9 | mpbiri 248 |
. . . . . . . . 9
|
11 | | fnrndomg 9358 |
. . . . . . . . 9
|
12 | 1, 10, 11 | mpsyl 68 |
. . . . . . . 8
|
13 | | domsdomtr 8095 |
. . . . . . . 8
|
14 | 12, 13 | sylan 488 |
. . . . . . 7
|
15 | | sdomdif 8108 |
. . . . . . 7
|
16 | 14, 15 | syl 17 |
. . . . . 6
|
17 | 16 | ralimiaa 2951 |
. . . . 5
|
18 | | konigth.1 |
. . . . . 6
|
19 | | fvex 6201 |
. . . . . . 7
|
20 | | difss 3737 |
. . . . . . 7
|
21 | 19, 20 | ssexi 4803 |
. . . . . 6
|
22 | 18, 21 | ac6c5 9304 |
. . . . 5
|
23 | | equid 1939 |
. . . . . . 7
|
24 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
25 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
26 | | konigth.5 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
|
28 | 25, 27 | mpan2 707 |
. . . . . . . . . . . . . 14
|
29 | 28 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
30 | 24, 29 | syl5ibr 236 |
. . . . . . . . . . . 12
|
31 | 30 | ralimia 2950 |
. . . . . . . . . . 11
|
32 | 25, 26 | fnmpti 6022 |
. . . . . . . . . . 11
|
33 | 31, 32 | jctil 560 |
. . . . . . . . . 10
|
34 | 18 | mptex 6486 |
. . . . . . . . . . . 12
|
35 | 26, 34 | eqeltri 2697 |
. . . . . . . . . . 11
|
36 | 35 | elixp 7915 |
. . . . . . . . . 10
|
37 | 33, 36 | sylibr 224 |
. . . . . . . . 9
|
38 | | konigth.3 |
. . . . . . . . 9
|
39 | 37, 38 | syl6eleqr 2712 |
. . . . . . . 8
|
40 | | foelrn 6378 |
. . . . . . . . . 10
|
41 | 40 | expcom 451 |
. . . . . . . . 9
|
42 | | konigth.2 |
. . . . . . . . . . . . . . 15
|
43 | 42 | eleq2i 2693 |
. . . . . . . . . . . . . 14
|
44 | | eliun 4524 |
. . . . . . . . . . . . . 14
|
45 | 43, 44 | bitri 264 |
. . . . . . . . . . . . 13
|
46 | | nfra1 2941 |
. . . . . . . . . . . . . . 15
|
47 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | nfan 1828 |
. . . . . . . . . . . . . 14
|
49 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
50 | 28 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 8 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | 3 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
54 | 2, 53 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | 52, 54 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 55 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 51, 56 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 50, 57 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
59 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | 10, 59 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 58, 61 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
63 | 62 | 3adant1 1079 |
. . . . . . . . . . . . . . . . 17
|
64 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
|
65 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . 18
|
66 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . 19
|
67 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 66, 67 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
|
69 | 64, 65, 68 | sylc 65 |
. . . . . . . . . . . . . . . . 17
|
70 | 63, 69 | pm2.21dd 186 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | 3expia 1267 |
. . . . . . . . . . . . . . 15
|
72 | 71 | expd 452 |
. . . . . . . . . . . . . 14
|
73 | 48, 49, 72 | rexlimd 3026 |
. . . . . . . . . . . . 13
|
74 | 45, 73 | syl5bi 232 |
. . . . . . . . . . . 12
|
75 | 74 | ex 450 |
. . . . . . . . . . 11
|
76 | 75 | com23 86 |
. . . . . . . . . 10
|
77 | 76 | rexlimdv 3030 |
. . . . . . . . 9
|
78 | 41, 77 | syl9r 78 |
. . . . . . . 8
|
79 | 39, 78 | mpd 15 |
. . . . . . 7
|
80 | 23, 79 | mt2i 132 |
. . . . . 6
|
81 | 80 | exlimiv 1858 |
. . . . 5
|
82 | 17, 22, 81 | 3syl 18 |
. . . 4
|
83 | 82 | nexdv 1864 |
. . 3
|
84 | 1 | 0dom 8090 |
. . . . . . . 8
|
85 | | domsdomtr 8095 |
. . . . . . . 8
|
86 | 84, 85 | mpan 706 |
. . . . . . 7
|
87 | 19 | 0sdom 8091 |
. . . . . . 7
|
88 | 86, 87 | sylib 208 |
. . . . . 6
|
89 | 88 | ralimi 2952 |
. . . . 5
|
90 | 38 | neeq1i 2858 |
. . . . . 6
|
91 | 19 | rgenw 2924 |
. . . . . . . . 9
|
92 | | ixpexg 7932 |
. . . . . . . . 9
|
93 | 91, 92 | ax-mp 5 |
. . . . . . . 8
|
94 | 38, 93 | eqeltri 2697 |
. . . . . . 7
|
95 | 94 | 0sdom 8091 |
. . . . . 6
|
96 | 18, 19 | ac9 9305 |
. . . . . 6
|
97 | 90, 95, 96 | 3bitr4i 292 |
. . . . 5
|
98 | 89, 97 | sylibr 224 |
. . . 4
|
99 | 18, 1 | iunex 7147 |
. . . . . . 7
|
100 | 42, 99 | eqeltri 2697 |
. . . . . 6
|
101 | | domtri 9378 |
. . . . . 6
|
102 | 94, 100, 101 | mp2an 708 |
. . . . 5
|
103 | 102 | biimpri 218 |
. . . 4
|
104 | | fodomr 8111 |
. . . 4
|
105 | 98, 103, 104 | syl2an 494 |
. . 3
|
106 | 83, 105 | mtand 691 |
. 2
|
107 | 106 | notnotrd 128 |
1
|