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

Theorem subctctexmid 13533
 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 4550 . . . . . . . 8 ω ∈ V
32rabex 4108 . . . . . . 7 {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V
43a1i 9 . . . . . 6 (𝜑 → {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V)
5 ssrab2 3213 . . . . . . 7 {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω
6 f1oi 5449 . . . . . . . . 9 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
7 f1ofo 5418 . . . . . . . . 9 (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
86, 7ax-mp 5 . . . . . . . 8 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
9 resiexg 4908 . . . . . . . . . 10 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V)
103, 9ax-mp 5 . . . . . . . . 9 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V
11 foeq1 5385 . . . . . . . . 9 (𝑓 = ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) → (𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1210, 11spcev 2807 . . . . . . . 8 (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
138, 12ax-mp 5 . . . . . . 7 𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
145, 13pm3.2i 270 . . . . . 6 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
15 sseq1 3151 . . . . . . . 8 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑠 ⊆ ω ↔ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω))
16 foeq2 5386 . . . . . . . . 9 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1716exbidv 1805 . . . . . . . 8 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1815, 17anbi12d 465 . . . . . . 7 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) ↔ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
1918spcegv 2800 . . . . . 6 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → (({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
204, 14, 19mpisyl 1426 . . . . 5 (𝜑 → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
21 foeq3 5387 . . . . . . . . . 10 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠onto𝑥𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
2221exbidv 1805 . . . . . . . . 9 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠onto𝑥 ↔ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
2322anbi2d 460 . . . . . . . 8 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) ↔ (𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
2423exbidv 1805 . . . . . . 7 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) ↔ ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
25 djueq1 6974 . . . . . . . . 9 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑥 ⊔ 1o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
26 foeq3 5387 . . . . . . . . 9 ((𝑥 ⊔ 1o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → (𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2725, 26syl 14 . . . . . . . 8 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2827exbidv 1805 . . . . . . 7 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2924, 28imbi12d 233 . . . . . 6 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o)) ↔ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))))
303, 29spcv 2806 . . . . 5 (∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o)) → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
311, 20, 30sylc 62 . . . 4 (𝜑 → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
32 fveq1 5464 . . . . . . . . . . . 12 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → (𝑛) = ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛))
3332eqeq1d 2166 . . . . . . . . . . 11 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → ((𝑛) = 1o ↔ ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
3433rexbidv 2458 . . . . . . . . . 10 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → (∃𝑛 ∈ ω (𝑛) = 1o ↔ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
3534notbid 657 . . . . . . . . 9 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → (¬ ∃𝑛 ∈ ω (𝑛) = 1o ↔ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
3635notbid 657 . . . . . . . 8 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → (¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o ↔ ¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
3736, 34imbi12d 233 . . . . . . 7 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → ((¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o) ↔ (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o)))
38 subctctexmid.mk . . . . . . . . 9 (𝜑 → ω ∈ Markov)
39 ismkvnex 7081 . . . . . . . . . 10 (ω ∈ Markov → (ω ∈ Markov ↔ ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o)))
4038, 39syl 14 . . . . . . . . 9 (𝜑 → (ω ∈ Markov ↔ ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o)))
4138, 40mpbid 146 . . . . . . . 8 (𝜑 → ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o))
4241adantr 274 . . . . . . 7 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o))
43 1lt2o 6383 . . . . . . . . . . . 12 1o ∈ 2o
4443a1i 9 . . . . . . . . . . 11 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ (1st ‘(𝑔𝑛)) = ∅) → 1o ∈ 2o)
45 0lt2o 6382 . . . . . . . . . . . 12 ∅ ∈ 2o
4645a1i 9 . . . . . . . . . . 11 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ ¬ (1st ‘(𝑔𝑛)) = ∅) → ∅ ∈ 2o)
47 simplr 520 . . . . . . . . . . . . . . 15 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
48 fof 5389 . . . . . . . . . . . . . . 15 (𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
4947, 48syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
50 simpr 109 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
5149, 50ffvelrnd 5600 . . . . . . . . . . . . 13 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
52 eldju1st 7005 . . . . . . . . . . . . 13 ((𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → ((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o))
5351, 52syl 14 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → ((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o))
54 1n0 6373 . . . . . . . . . . . . . . . 16 1o ≠ ∅
5554neii 2329 . . . . . . . . . . . . . . 15 ¬ 1o = ∅
56 eqeq1 2164 . . . . . . . . . . . . . . 15 ((1st ‘(𝑔𝑛)) = 1o → ((1st ‘(𝑔𝑛)) = ∅ ↔ 1o = ∅))
5755, 56mtbiri 665 . . . . . . . . . . . . . 14 ((1st ‘(𝑔𝑛)) = 1o → ¬ (1st ‘(𝑔𝑛)) = ∅)
5857orim2i 751 . . . . . . . . . . . . 13 (((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o) → ((1st ‘(𝑔𝑛)) = ∅ ∨ ¬ (1st ‘(𝑔𝑛)) = ∅))
59 df-dc 821 . . . . . . . . . . . . 13 (DECID (1st ‘(𝑔𝑛)) = ∅ ↔ ((1st ‘(𝑔𝑛)) = ∅ ∨ ¬ (1st ‘(𝑔𝑛)) = ∅))
6058, 59sylibr 133 . . . . . . . . . . . 12 (((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o) → DECID (1st ‘(𝑔𝑛)) = ∅)
6153, 60syl 14 . . . . . . . . . . 11 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → DECID (1st ‘(𝑔𝑛)) = ∅)
6244, 46, 61ifcldadc 3534 . . . . . . . . . 10 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ∈ 2o)
6362fmpttd 5619 . . . . . . . . 9 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)):ω⟶2o)
64 2fveq3 5470 . . . . . . . . . . . . . 14 (𝑤 = 𝑛 → (1st ‘(𝑔𝑤)) = (1st ‘(𝑔𝑛)))
6564eqeq1d 2166 . . . . . . . . . . . . 13 (𝑤 = 𝑛 → ((1st ‘(𝑔𝑤)) = ∅ ↔ (1st ‘(𝑔𝑛)) = ∅))
6665ifbid 3526 . . . . . . . . . . . 12 (𝑤 = 𝑛 → if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
67 eqcom 2159 . . . . . . . . . . . 12 (𝑤 = 𝑛𝑛 = 𝑤)
68 eqcom 2159 . . . . . . . . . . . 12 (if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
6966, 67, 683imtr3i 199 . . . . . . . . . . 11 (𝑛 = 𝑤 → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7069cbvmptv 4060 . . . . . . . . . 10 (𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)) = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7170feq1i 5309 . . . . . . . . 9 ((𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)):ω⟶2o ↔ (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
7263, 71sylib 121 . . . . . . . 8 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
73 2onn 6461 . . . . . . . . . 10 2o ∈ ω
7473elexi 2724 . . . . . . . . 9 2o ∈ V
7574, 2elmap 6615 . . . . . . . 8 ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) ∈ (2o𝑚 ω) ↔ (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
7672, 75sylibr 133 . . . . . . 7 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) ∈ (2o𝑚 ω))
7737, 42, 76rspcdva 2821 . . . . . 6 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
78 eqid 2157 . . . . . . . . . . . . 13 (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7978, 66, 50, 62fvmptd3 5558 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
8079eqeq1d 2166 . . . . . . . . . . 11 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o ↔ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o))
8151adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
82 simpr 109 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o)
8382eqcomd 2163 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → 1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
84 eqifdc 3539 . . . . . . . . . . . . . . . . . . 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 2157 . . . . . . . . . . . . . . . . . . 19 1o = 1o
87 orcom 718 . . . . . . . . . . . . . . . . . . . 20 ((((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o) ∨ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)) ↔ ((¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅) ∨ ((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o)))
8855intnan 915 . . . . . . . . . . . . . . . . . . . . 21 ¬ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)
89 biorf 734 . . . . . . . . . . . . . . . . . . . . 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 186 . . . . . . . . . . . . . . . . . . 19 ((((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o) ∨ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)) ↔ ((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o))
9286, 91mpbiran2 926 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o) ∨ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)) ↔ (1st ‘(𝑔𝑛)) = ∅)
9385, 92bitrdi 195 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ (1st ‘(𝑔𝑛)) = ∅))
9493adantr 274 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ (1st ‘(𝑔𝑛)) = ∅))
9583, 94mpbid 146 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (1st ‘(𝑔𝑛)) = ∅)
96 eldju2ndl 7006 . . . . . . . . . . . . . . 15 (((𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) ∧ (1st ‘(𝑔𝑛)) = ∅) → (2nd ‘(𝑔𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
9781, 95, 96syl2anc 409 . . . . . . . . . . . . . 14 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (2nd ‘(𝑔𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
98 biidd 171 . . . . . . . . . . . . . . 15 (𝑧 = (2nd ‘(𝑔𝑛)) → (𝑦 = {∅} ↔ 𝑦 = {∅}))
9998elrab 2868 . . . . . . . . . . . . . 14 ((2nd ‘(𝑔𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ((2nd ‘(𝑔𝑛)) ∈ ω ∧ 𝑦 = {∅}))
10097, 99sylib 121 . . . . . . . . . . . . 13 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → ((2nd ‘(𝑔𝑛)) ∈ ω ∧ 𝑦 = {∅}))
101100simprd 113 . . . . . . . . . . . 12 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → 𝑦 = {∅})
102101ex 114 . . . . . . . . . . 11 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o𝑦 = {∅}))
10380, 102sylbid 149 . . . . . . . . . 10 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o𝑦 = {∅}))
104103rexlimdva 2574 . . . . . . . . 9 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o𝑦 = {∅}))
105 simplr 520 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
106 biidd 171 . . . . . . . . . . . . . 14 (𝑧 = ∅ → (𝑦 = {∅} ↔ 𝑦 = {∅}))
107 peano1 4551 . . . . . . . . . . . . . . 15 ∅ ∈ ω
108107a1i 9 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∅ ∈ ω)
109 simpr 109 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
110106, 108, 109elrabd 2870 . . . . . . . . . . . . 13 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
111 djulcl 6985 . . . . . . . . . . . . 13 (∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
112110, 111syl 14 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
113 foelrn 5698 . . . . . . . . . . . 12 ((𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) ∧ (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → ∃𝑛 ∈ ω (inl‘∅) = (𝑔𝑛))
114105, 112, 113syl2anc 409 . . . . . . . . . . 11 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∃𝑛 ∈ ω (inl‘∅) = (𝑔𝑛))
11579adantlr 469 . . . . . . . . . . . . . 14 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
116 1stinl 7008 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (1st ‘(inl‘∅)) = ∅)
117107, 116ax-mp 5 . . . . . . . . . . . . . . . 16 (1st ‘(inl‘∅)) = ∅
118 fveq2 5465 . . . . . . . . . . . . . . . 16 ((inl‘∅) = (𝑔𝑛) → (1st ‘(inl‘∅)) = (1st ‘(𝑔𝑛)))
119117, 118syl5reqr 2205 . . . . . . . . . . . . . . 15 ((inl‘∅) = (𝑔𝑛) → (1st ‘(𝑔𝑛)) = ∅)
120119iftrued 3512 . . . . . . . . . . . . . 14 ((inl‘∅) = (𝑔𝑛) → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o)
121115, 120sylan9eq 2210 . . . . . . . . . . . . 13 (((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) ∧ (inl‘∅) = (𝑔𝑛)) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o)
122121ex 114 . . . . . . . . . . . 12 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) → ((inl‘∅) = (𝑔𝑛) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
123122reximdva 2559 . . . . . . . . . . 11 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → (∃𝑛 ∈ ω (inl‘∅) = (𝑔𝑛) → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
124114, 123mpd 13 . . . . . . . . . 10 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o)
125124ex 114 . . . . . . . . 9 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑦 = {∅} → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
126104, 125impbid 128 . . . . . . . 8 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o𝑦 = {∅}))
127126notbid 657 . . . . . . 7 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o ↔ ¬ 𝑦 = {∅}))
128127notbid 657 . . . . . 6 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o ↔ ¬ ¬ 𝑦 = {∅}))
12977, 128, 1263imtr3d 201 . . . . 5 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
130 df-stab 817 . . . . 5 (STAB 𝑦 = {∅} ↔ (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
131129, 130sylibr 133 . . . 4 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → STAB 𝑦 = {∅})
13231, 131exlimddv 1878 . . 3 (𝜑STAB 𝑦 = {∅})
133132adantr 274 . 2 ((𝜑𝑦 ⊆ {∅}) → STAB 𝑦 = {∅})
134133exmid1stab 13532 1 (𝜑EXMID)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  STAB wstab 816  DECID wdc 820  ∀wal 1333   = wceq 1335  ∃wex 1472   ∈ wcel 2128  ∀wral 2435  ∃wrex 2436  {crab 2439  Vcvv 2712   ⊆ wss 3102  ∅c0 3394  ifcif 3505  {csn 3560   ↦ cmpt 4025  EXMIDwem 4154   I cid 4247  ωcom 4547   ↾ cres 4585  ⟶wf 5163  –onto→wfo 5165  –1-1-onto→wf1o 5166  ‘cfv 5167  (class class class)co 5818  1st c1st 6080  2nd c2nd 6081  1oc1o 6350  2oc2o 6351   ↑𝑚 cmap 6586   ⊔ cdju 6971  inlcinl 6979  Markovcmarkov 7077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-exmid 4155  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-1o 6357  df-2o 6358  df-map 6588  df-dju 6972  df-inl 6981  df-inr 6982  df-markov 7078 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator