Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  subctctexmid Unicode version

Theorem subctctexmid 13520
 Description: If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.)
Hypotheses
Ref Expression
subctctexmid.x
subctctexmid.mk Markov
Assertion
Ref Expression
subctctexmid EXMID
Distinct variable groups:   ,,   ,   ,
Allowed substitution hints:   (,,)

Proof of Theorem subctctexmid
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subctctexmid.x . . . . 5
2 omex 4546 . . . . . . . 8
32rabex 4104 . . . . . . 7
43a1i 9 . . . . . 6
5 ssrab2 3209 . . . . . . 7
6 f1oi 5445 . . . . . . . . 9
7 f1ofo 5414 . . . . . . . . 9
86, 7ax-mp 5 . . . . . . . 8
9 resiexg 4904 . . . . . . . . . 10
103, 9ax-mp 5 . . . . . . . . 9
11 foeq1 5381 . . . . . . . . 9
1210, 11spcev 2804 . . . . . . . 8
138, 12ax-mp 5 . . . . . . 7
145, 13pm3.2i 270 . . . . . 6
15 sseq1 3147 . . . . . . . 8
16 foeq2 5382 . . . . . . . . 9
1716exbidv 1802 . . . . . . . 8
1815, 17anbi12d 465 . . . . . . 7
1918spcegv 2797 . . . . . 6
204, 14, 19mpisyl 1423 . . . . 5
21 foeq3 5383 . . . . . . . . . 10
2221exbidv 1802 . . . . . . . . 9
2322anbi2d 460 . . . . . . . 8
2423exbidv 1802 . . . . . . 7
25 djueq1 6970 . . . . . . . . 9
26 foeq3 5383 . . . . . . . . 9
2725, 26syl 14 . . . . . . . 8
2827exbidv 1802 . . . . . . 7
2924, 28imbi12d 233 . . . . . 6
303, 29spcv 2803 . . . . 5
311, 20, 30sylc 62 . . . 4
32 fveq1 5460 . . . . . . . . . . . 12
3332eqeq1d 2163 . . . . . . . . . . 11
3433rexbidv 2455 . . . . . . . . . 10
3534notbid 657 . . . . . . . . 9
3635notbid 657 . . . . . . . 8
3736, 34imbi12d 233 . . . . . . 7
38 subctctexmid.mk . . . . . . . . 9 Markov
39 ismkvnex 7077 . . . . . . . . . 10 Markov Markov
4038, 39syl 14 . . . . . . . . 9 Markov
4138, 40mpbid 146 . . . . . . . 8
4241adantr 274 . . . . . . 7
43 1lt2o 6379 . . . . . . . . . . . 12
4443a1i 9 . . . . . . . . . . 11
45 0lt2o 6378 . . . . . . . . . . . 12
4645a1i 9 . . . . . . . . . . 11
47 simplr 520 . . . . . . . . . . . . . . 15
48 fof 5385 . . . . . . . . . . . . . . 15
4947, 48syl 14 . . . . . . . . . . . . . 14
50 simpr 109 . . . . . . . . . . . . . 14
5149, 50ffvelrnd 5596 . . . . . . . . . . . . 13
52 eldju1st 7001 . . . . . . . . . . . . 13
5351, 52syl 14 . . . . . . . . . . . 12
54 1n0 6369 . . . . . . . . . . . . . . . 16
5554neii 2326 . . . . . . . . . . . . . . 15
56 eqeq1 2161 . . . . . . . . . . . . . . 15
5755, 56mtbiri 665 . . . . . . . . . . . . . 14
5857orim2i 751 . . . . . . . . . . . . 13
59 df-dc 821 . . . . . . . . . . . . 13 DECID
6058, 59sylibr 133 . . . . . . . . . . . 12 DECID
6153, 60syl 14 . . . . . . . . . . 11 DECID
6244, 46, 61ifcldadc 3530 . . . . . . . . . 10
6362fmpttd 5615 . . . . . . . . 9
64 2fveq3 5466 . . . . . . . . . . . . . 14
6564eqeq1d 2163 . . . . . . . . . . . . 13
6665ifbid 3522 . . . . . . . . . . . 12
67 eqcom 2156 . . . . . . . . . . . 12
68 eqcom 2156 . . . . . . . . . . . 12
6966, 67, 683imtr3i 199 . . . . . . . . . . 11
7069cbvmptv 4056 . . . . . . . . . 10
7170feq1i 5305 . . . . . . . . 9
7263, 71sylib 121 . . . . . . . 8
73 2onn 6457 . . . . . . . . . 10
7473elexi 2721 . . . . . . . . 9
7574, 2elmap 6611 . . . . . . . 8
7672, 75sylibr 133 . . . . . . 7
7737, 42, 76rspcdva 2818 . . . . . 6
78 eqid 2154 . . . . . . . . . . . . 13
7978, 66, 50, 62fvmptd3 5554 . . . . . . . . . . . 12
8079eqeq1d 2163 . . . . . . . . . . 11
8151adantr 274 . . . . . . . . . . . . . . 15
82 simpr 109 . . . . . . . . . . . . . . . . 17
8382eqcomd 2160 . . . . . . . . . . . . . . . 16
84 eqifdc 3535 . . . . . . . . . . . . . . . . . . 19 DECID
8561, 84syl 14 . . . . . . . . . . . . . . . . . 18
86 eqid 2154 . . . . . . . . . . . . . . . . . . 19
87 orcom 718 . . . . . . . . . . . . . . . . . . . 20
8855intnan 915 . . . . . . . . . . . . . . . . . . . . 21
89 biorf 734 . . . . . . . . . . . . . . . . . . . . 21
9088, 89ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
9187, 90bitr4i 186 . . . . . . . . . . . . . . . . . . 19
9286, 91mpbiran2 926 . . . . . . . . . . . . . . . . . 18
9385, 92bitrdi 195 . . . . . . . . . . . . . . . . 17
9493adantr 274 . . . . . . . . . . . . . . . 16
9583, 94mpbid 146 . . . . . . . . . . . . . . 15
96 eldju2ndl 7002 . . . . . . . . . . . . . . 15
9781, 95, 96syl2anc 409 . . . . . . . . . . . . . 14
98 biidd 171 . . . . . . . . . . . . . . 15
9998elrab 2864 . . . . . . . . . . . . . 14
10097, 99sylib 121 . . . . . . . . . . . . 13
101100simprd 113 . . . . . . . . . . . 12
102101ex 114 . . . . . . . . . . 11
10380, 102sylbid 149 . . . . . . . . . 10
104103rexlimdva 2571 . . . . . . . . 9
105 simplr 520 . . . . . . . . . . . 12
106 biidd 171 . . . . . . . . . . . . . 14
107 peano1 4547 . . . . . . . . . . . . . . 15
108107a1i 9 . . . . . . . . . . . . . 14
109 simpr 109 . . . . . . . . . . . . . 14
110106, 108, 109elrabd 2866 . . . . . . . . . . . . 13
111 djulcl 6981 . . . . . . . . . . . . 13 inl
112110, 111syl 14 . . . . . . . . . . . 12 inl
113 foelrn 5694 . . . . . . . . . . . 12 inl inl
114105, 112, 113syl2anc 409 . . . . . . . . . . 11 inl
11579adantlr 469 . . . . . . . . . . . . . 14
116 1stinl 7004 . . . . . . . . . . . . . . . . 17 inl
117107, 116ax-mp 5 . . . . . . . . . . . . . . . 16 inl
118 fveq2 5461 . . . . . . . . . . . . . . . 16 inl inl
119117, 118syl5reqr 2202 . . . . . . . . . . . . . . 15 inl
120119iftrued 3508 . . . . . . . . . . . . . 14 inl
121115, 120sylan9eq 2207 . . . . . . . . . . . . 13 inl
122121ex 114 . . . . . . . . . . . 12 inl
123122reximdva 2556 . . . . . . . . . . 11 inl
124114, 123mpd 13 . . . . . . . . . 10
125124ex 114 . . . . . . . . 9
126104, 125impbid 128 . . . . . . . 8
127126notbid 657 . . . . . . 7
128127notbid 657 . . . . . 6
12977, 128, 1263imtr3d 201 . . . . 5
130 df-stab 817 . . . . 5 STAB
131129, 130sylibr 133 . . . 4 STAB
13231, 131exlimddv 1875 . . 3 STAB