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

Theorem subctctexmid 14233
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 (πœ‘ β†’ βˆ€π‘₯(βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o)))
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 (πœ‘ β†’ βˆ€π‘₯(βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o)))
2 omex 4586 . . . . . . . 8 Ο‰ ∈ V
32rabex 4142 . . . . . . 7 {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ∈ V
43a1i 9 . . . . . 6 (πœ‘ β†’ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ∈ V)
5 ssrab2 3238 . . . . . . 7 {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ† Ο‰
6 f1oi 5491 . . . . . . . . 9 ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–1-1-ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}
7 f1ofo 5460 . . . . . . . . 9 (( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–1-1-ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
86, 7ax-mp 5 . . . . . . . 8 ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}
9 resiexg 4945 . . . . . . . . . 10 ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ∈ V β†’ ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) ∈ V)
103, 9ax-mp 5 . . . . . . . . 9 ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) ∈ V
11 foeq1 5426 . . . . . . . . 9 (𝑓 = ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) β†’ (𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ↔ ( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
1210, 11spcev 2830 . . . . . . . 8 (( I β†Ύ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}):{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
138, 12ax-mp 5 . . . . . . 7 βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}
145, 13pm3.2i 272 . . . . . 6 ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
15 sseq1 3176 . . . . . . . 8 (𝑠 = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (𝑠 βŠ† Ο‰ ↔ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ† Ο‰))
16 foeq2 5427 . . . . . . . . 9 (𝑠 = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ↔ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
1716exbidv 1823 . . . . . . . 8 (𝑠 = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ↔ βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
1815, 17anbi12d 473 . . . . . . 7 (𝑠 = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ ((𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) ↔ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})))
1918spcegv 2823 . . . . . 6 ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ∈ V β†’ (({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) β†’ βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})))
204, 14, 19mpisyl 1444 . . . . 5 (πœ‘ β†’ βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
21 foeq3 5428 . . . . . . . . . 10 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (𝑓:𝑠–ontoβ†’π‘₯ ↔ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
2221exbidv 1823 . . . . . . . . 9 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯ ↔ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}))
2322anbi2d 464 . . . . . . . 8 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ ((𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) ↔ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})))
2423exbidv 1823 . . . . . . 7 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) ↔ βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})))
25 djueq1 7029 . . . . . . . . 9 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (π‘₯ βŠ” 1o) = ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
26 foeq3 5428 . . . . . . . . 9 ((π‘₯ βŠ” 1o) = ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o) β†’ (𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o) ↔ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)))
2725, 26syl 14 . . . . . . . 8 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o) ↔ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)))
2827exbidv 1823 . . . . . . 7 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (βˆƒπ‘” 𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o) ↔ βˆƒπ‘” 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)))
2924, 28imbi12d 235 . . . . . 6 (π‘₯ = {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ ((βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o)) ↔ (βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))))
303, 29spcv 2829 . . . . 5 (βˆ€π‘₯(βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’π‘₯) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’(π‘₯ βŠ” 1o)) β†’ (βˆƒπ‘ (𝑠 βŠ† Ο‰ ∧ βˆƒπ‘“ 𝑓:𝑠–ontoβ†’{𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}}) β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)))
311, 20, 30sylc 62 . . . 4 (πœ‘ β†’ βˆƒπ‘” 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
32 fveq1 5506 . . . . . . . . . . . 12 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ (β„Žβ€˜π‘›) = ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›))
3332eqeq1d 2184 . . . . . . . . . . 11 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ ((β„Žβ€˜π‘›) = 1o ↔ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
3433rexbidv 2476 . . . . . . . . . 10 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ (βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o ↔ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
3534notbid 667 . . . . . . . . 9 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ (Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o ↔ Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
3635notbid 667 . . . . . . . 8 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ (Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o ↔ Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
3736, 34imbi12d 235 . . . . . . 7 (β„Ž = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) β†’ ((Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o) ↔ (Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o)))
38 subctctexmid.mk . . . . . . . . 9 (πœ‘ β†’ Ο‰ ∈ Markov)
39 ismkvnex 7143 . . . . . . . . . 10 (Ο‰ ∈ Markov β†’ (Ο‰ ∈ Markov ↔ βˆ€β„Ž ∈ (2o β†‘π‘š Ο‰)(Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o)))
4038, 39syl 14 . . . . . . . . 9 (πœ‘ β†’ (Ο‰ ∈ Markov ↔ βˆ€β„Ž ∈ (2o β†‘π‘š Ο‰)(Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o)))
4138, 40mpbid 148 . . . . . . . 8 (πœ‘ β†’ βˆ€β„Ž ∈ (2o β†‘π‘š Ο‰)(Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o))
4241adantr 276 . . . . . . 7 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ βˆ€β„Ž ∈ (2o β†‘π‘š Ο‰)(Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ (β„Žβ€˜π‘›) = 1o))
43 1lt2o 6433 . . . . . . . . . . . 12 1o ∈ 2o
4443a1i 9 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ (1st β€˜(π‘”β€˜π‘›)) = βˆ…) β†’ 1o ∈ 2o)
45 0lt2o 6432 . . . . . . . . . . . 12 βˆ… ∈ 2o
4645a1i 9 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ…) β†’ βˆ… ∈ 2o)
47 simplr 528 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
48 fof 5430 . . . . . . . . . . . . . . 15 (𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o) β†’ 𝑔:Ο‰βŸΆ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
4947, 48syl 14 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ 𝑔:Ο‰βŸΆ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
50 simpr 110 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ 𝑛 ∈ Ο‰)
5149, 50ffvelrnd 5644 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (π‘”β€˜π‘›) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
52 eldju1st 7060 . . . . . . . . . . . . 13 ((π‘”β€˜π‘›) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o) β†’ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ (1st β€˜(π‘”β€˜π‘›)) = 1o))
5351, 52syl 14 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ (1st β€˜(π‘”β€˜π‘›)) = 1o))
54 1n0 6423 . . . . . . . . . . . . . . . 16 1o β‰  βˆ…
5554neii 2347 . . . . . . . . . . . . . . 15 Β¬ 1o = βˆ…
56 eqeq1 2182 . . . . . . . . . . . . . . 15 ((1st β€˜(π‘”β€˜π‘›)) = 1o β†’ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ↔ 1o = βˆ…))
5755, 56mtbiri 675 . . . . . . . . . . . . . 14 ((1st β€˜(π‘”β€˜π‘›)) = 1o β†’ Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
5857orim2i 761 . . . . . . . . . . . . 13 (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ (1st β€˜(π‘”β€˜π‘›)) = 1o) β†’ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ…))
59 df-dc 835 . . . . . . . . . . . . 13 (DECID (1st β€˜(π‘”β€˜π‘›)) = βˆ… ↔ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ…))
6058, 59sylibr 134 . . . . . . . . . . . 12 (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∨ (1st β€˜(π‘”β€˜π‘›)) = 1o) β†’ DECID (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
6153, 60syl 14 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ DECID (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
6244, 46, 61ifcldadc 3561 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ∈ 2o)
6362fmpttd 5663 . . . . . . . . 9 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (𝑛 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…)):Ο‰βŸΆ2o)
64 2fveq3 5512 . . . . . . . . . . . . . 14 (𝑀 = 𝑛 β†’ (1st β€˜(π‘”β€˜π‘€)) = (1st β€˜(π‘”β€˜π‘›)))
6564eqeq1d 2184 . . . . . . . . . . . . 13 (𝑀 = 𝑛 β†’ ((1st β€˜(π‘”β€˜π‘€)) = βˆ… ↔ (1st β€˜(π‘”β€˜π‘›)) = βˆ…))
6665ifbid 3553 . . . . . . . . . . . 12 (𝑀 = 𝑛 β†’ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…) = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…))
67 eqcom 2177 . . . . . . . . . . . 12 (𝑀 = 𝑛 ↔ 𝑛 = 𝑀)
68 eqcom 2177 . . . . . . . . . . . 12 (if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…) = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ↔ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))
6966, 67, 683imtr3i 201 . . . . . . . . . . 11 (𝑛 = 𝑀 β†’ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))
7069cbvmptv 4094 . . . . . . . . . 10 (𝑛 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…)) = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))
7170feq1i 5350 . . . . . . . . 9 ((𝑛 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…)):Ο‰βŸΆ2o ↔ (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)):Ο‰βŸΆ2o)
7263, 71sylib 122 . . . . . . . 8 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)):Ο‰βŸΆ2o)
73 2onn 6512 . . . . . . . . . 10 2o ∈ Ο‰
7473elexi 2747 . . . . . . . . 9 2o ∈ V
7574, 2elmap 6667 . . . . . . . 8 ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) ∈ (2o β†‘π‘š Ο‰) ↔ (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)):Ο‰βŸΆ2o)
7672, 75sylibr 134 . . . . . . 7 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) ∈ (2o β†‘π‘š Ο‰))
7737, 42, 76rspcdva 2844 . . . . . 6 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o β†’ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
78 eqid 2175 . . . . . . . . . . . . 13 (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…)) = (𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))
7978, 66, 50, 62fvmptd3 5601 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…))
8079eqeq1d 2184 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o ↔ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o))
8151adantr 276 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ (π‘”β€˜π‘›) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
82 simpr 110 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o)
8382eqcomd 2181 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ 1o = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…))
84 eqifdc 3566 . . . . . . . . . . . . . . . . . . 19 (DECID (1st β€˜(π‘”β€˜π‘›)) = βˆ… β†’ (1o = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ↔ (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ∨ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…))))
8561, 84syl 14 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (1o = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ↔ (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ∨ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…))))
86 eqid 2175 . . . . . . . . . . . . . . . . . . 19 1o = 1o
87 orcom 728 . . . . . . . . . . . . . . . . . . . 20 ((((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ∨ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…)) ↔ ((Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…) ∨ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o)))
8855intnan 929 . . . . . . . . . . . . . . . . . . . . 21 Β¬ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…)
89 biorf 744 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…) β†’ (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ↔ ((Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…) ∨ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o))))
9088, 89ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ↔ ((Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…) ∨ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o)))
9187, 90bitr4i 188 . . . . . . . . . . . . . . . . . . 19 ((((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ∨ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…)) ↔ ((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o))
9286, 91mpbiran2 941 . . . . . . . . . . . . . . . . . 18 ((((1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = 1o) ∨ (Β¬ (1st β€˜(π‘”β€˜π‘›)) = βˆ… ∧ 1o = βˆ…)) ↔ (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
9385, 92bitrdi 197 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (1o = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ↔ (1st β€˜(π‘”β€˜π‘›)) = βˆ…))
9493adantr 276 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ (1o = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) ↔ (1st β€˜(π‘”β€˜π‘›)) = βˆ…))
9583, 94mpbid 148 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
96 eldju2ndl 7061 . . . . . . . . . . . . . . 15 (((π‘”β€˜π‘›) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o) ∧ (1st β€˜(π‘”β€˜π‘›)) = βˆ…) β†’ (2nd β€˜(π‘”β€˜π‘›)) ∈ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
9781, 95, 96syl2anc 411 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ (2nd β€˜(π‘”β€˜π‘›)) ∈ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
98 biidd 173 . . . . . . . . . . . . . . 15 (𝑧 = (2nd β€˜(π‘”β€˜π‘›)) β†’ (𝑦 = {βˆ…} ↔ 𝑦 = {βˆ…}))
9998elrab 2891 . . . . . . . . . . . . . 14 ((2nd β€˜(π‘”β€˜π‘›)) ∈ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} ↔ ((2nd β€˜(π‘”β€˜π‘›)) ∈ Ο‰ ∧ 𝑦 = {βˆ…}))
10097, 99sylib 122 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ ((2nd β€˜(π‘”β€˜π‘›)) ∈ Ο‰ ∧ 𝑦 = {βˆ…}))
101100simprd 114 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) ∧ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o) β†’ 𝑦 = {βˆ…})
102101ex 115 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o β†’ 𝑦 = {βˆ…}))
10380, 102sylbid 151 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑛 ∈ Ο‰) β†’ (((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o β†’ 𝑦 = {βˆ…}))
104103rexlimdva 2592 . . . . . . . . 9 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o β†’ 𝑦 = {βˆ…}))
105 simplr 528 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
106 biidd 173 . . . . . . . . . . . . . 14 (𝑧 = βˆ… β†’ (𝑦 = {βˆ…} ↔ 𝑦 = {βˆ…}))
107 peano1 4587 . . . . . . . . . . . . . . 15 βˆ… ∈ Ο‰
108107a1i 9 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ βˆ… ∈ Ο‰)
109 simpr 110 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ 𝑦 = {βˆ…})
110106, 108, 109elrabd 2893 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ βˆ… ∈ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}})
111 djulcl 7040 . . . . . . . . . . . . 13 (βˆ… ∈ {𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} β†’ (inlβ€˜βˆ…) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
112110, 111syl 14 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ (inlβ€˜βˆ…) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o))
113 foelrn 5744 . . . . . . . . . . . 12 ((𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o) ∧ (inlβ€˜βˆ…) ∈ ({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ βˆƒπ‘› ∈ Ο‰ (inlβ€˜βˆ…) = (π‘”β€˜π‘›))
114105, 112, 113syl2anc 411 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ βˆƒπ‘› ∈ Ο‰ (inlβ€˜βˆ…) = (π‘”β€˜π‘›))
11579adantlr 477 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) ∧ 𝑛 ∈ Ο‰) β†’ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…))
116 fveq2 5507 . . . . . . . . . . . . . . . 16 ((inlβ€˜βˆ…) = (π‘”β€˜π‘›) β†’ (1st β€˜(inlβ€˜βˆ…)) = (1st β€˜(π‘”β€˜π‘›)))
117 1stinl 7063 . . . . . . . . . . . . . . . . 17 (βˆ… ∈ Ο‰ β†’ (1st β€˜(inlβ€˜βˆ…)) = βˆ…)
118107, 117ax-mp 5 . . . . . . . . . . . . . . . 16 (1st β€˜(inlβ€˜βˆ…)) = βˆ…
119116, 118eqtr3di 2223 . . . . . . . . . . . . . . 15 ((inlβ€˜βˆ…) = (π‘”β€˜π‘›) β†’ (1st β€˜(π‘”β€˜π‘›)) = βˆ…)
120119iftrued 3539 . . . . . . . . . . . . . 14 ((inlβ€˜βˆ…) = (π‘”β€˜π‘›) β†’ if((1st β€˜(π‘”β€˜π‘›)) = βˆ…, 1o, βˆ…) = 1o)
121115, 120sylan9eq 2228 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) ∧ 𝑛 ∈ Ο‰) ∧ (inlβ€˜βˆ…) = (π‘”β€˜π‘›)) β†’ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o)
122121ex 115 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) ∧ 𝑛 ∈ Ο‰) β†’ ((inlβ€˜βˆ…) = (π‘”β€˜π‘›) β†’ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
123122reximdva 2577 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ (βˆƒπ‘› ∈ Ο‰ (inlβ€˜βˆ…) = (π‘”β€˜π‘›) β†’ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
124114, 123mpd 13 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) ∧ 𝑦 = {βˆ…}) β†’ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o)
125124ex 115 . . . . . . . . 9 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (𝑦 = {βˆ…} β†’ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o))
126104, 125impbid 129 . . . . . . . 8 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o ↔ 𝑦 = {βˆ…}))
127126notbid 667 . . . . . . 7 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o ↔ Β¬ 𝑦 = {βˆ…}))
128127notbid 667 . . . . . 6 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (Β¬ Β¬ βˆƒπ‘› ∈ Ο‰ ((𝑀 ∈ Ο‰ ↦ if((1st β€˜(π‘”β€˜π‘€)) = βˆ…, 1o, βˆ…))β€˜π‘›) = 1o ↔ Β¬ Β¬ 𝑦 = {βˆ…}))
12977, 128, 1263imtr3d 203 . . . . 5 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ (Β¬ Β¬ 𝑦 = {βˆ…} β†’ 𝑦 = {βˆ…}))
130 df-stab 831 . . . . 5 (STAB 𝑦 = {βˆ…} ↔ (Β¬ Β¬ 𝑦 = {βˆ…} β†’ 𝑦 = {βˆ…}))
131129, 130sylibr 134 . . . 4 ((πœ‘ ∧ 𝑔:ω–ontoβ†’({𝑧 ∈ Ο‰ ∣ 𝑦 = {βˆ…}} βŠ” 1o)) β†’ STAB 𝑦 = {βˆ…})
13231, 131exlimddv 1896 . . 3 (πœ‘ β†’ STAB 𝑦 = {βˆ…})
133132adantr 276 . 2 ((πœ‘ ∧ 𝑦 βŠ† {βˆ…}) β†’ STAB 𝑦 = {βˆ…})
134133exmid1stab 14232 1 (πœ‘ β†’ EXMID)
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  STAB wstab 830  DECID wdc 834  βˆ€wal 1351   = wceq 1353  βˆƒwex 1490   ∈ wcel 2146  βˆ€wral 2453  βˆƒwrex 2454  {crab 2457  Vcvv 2735   βŠ† wss 3127  βˆ…c0 3420  ifcif 3532  {csn 3589   ↦ cmpt 4059  EXMIDwem 4189   I cid 4282  Ο‰com 4583   β†Ύ cres 4622  βŸΆwf 5204  β€“ontoβ†’wfo 5206  β€“1-1-ontoβ†’wf1o 5207  β€˜cfv 5208  (class class class)co 5865  1st c1st 6129  2nd c2nd 6130  1oc1o 6400  2oc2o 6401   β†‘π‘š cmap 6638   βŠ” cdju 7026  inlcinl 7034  Markovcmarkov 7139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-exmid 4190  df-id 4287  df-iord 4360  df-on 4362  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-1o 6407  df-2o 6408  df-map 6640  df-dju 7027  df-inl 7036  df-inr 7037  df-markov 7140
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator