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

Theorem subctctexmid 14406
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 4589 . . . . . . . 8 ω ∈ V
32rabex 4144 . . . . . . 7 {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V
43a1i 9 . . . . . 6 (𝜑 → {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V)
5 ssrab2 3240 . . . . . . 7 {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω
6 f1oi 5495 . . . . . . . . 9 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
7 f1ofo 5464 . . . . . . . . 9 (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
86, 7ax-mp 5 . . . . . . . 8 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
9 resiexg 4948 . . . . . . . . . 10 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V)
103, 9ax-mp 5 . . . . . . . . 9 ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V
11 foeq1 5430 . . . . . . . . 9 (𝑓 = ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) → (𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1210, 11spcev 2832 . . . . . . . 8 (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
138, 12ax-mp 5 . . . . . . 7 𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
145, 13pm3.2i 272 . . . . . 6 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
15 sseq1 3178 . . . . . . . 8 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑠 ⊆ ω ↔ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω))
16 foeq2 5431 . . . . . . . . 9 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1716exbidv 1825 . . . . . . . 8 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
1815, 17anbi12d 473 . . . . . . 7 (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) ↔ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
1918spcegv 2825 . . . . . 6 ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → (({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
204, 14, 19mpisyl 1446 . . . . 5 (𝜑 → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
21 foeq3 5432 . . . . . . . . . 10 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠onto𝑥𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
2221exbidv 1825 . . . . . . . . 9 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠onto𝑥 ↔ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
2322anbi2d 464 . . . . . . . 8 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) ↔ (𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
2423exbidv 1825 . . . . . . 7 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) ↔ ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
25 djueq1 7033 . . . . . . . . 9 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑥 ⊔ 1o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
26 foeq3 5432 . . . . . . . . 9 ((𝑥 ⊔ 1o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → (𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2725, 26syl 14 . . . . . . . 8 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2827exbidv 1825 . . . . . . 7 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
2924, 28imbi12d 234 . . . . . 6 (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o)) ↔ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))))
303, 29spcv 2831 . . . . 5 (∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o)) → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)))
311, 20, 30sylc 62 . . . 4 (𝜑 → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
32 fveq1 5510 . . . . . . . . . . . 12 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → (𝑛) = ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛))
3332eqeq1d 2186 . . . . . . . . . . 11 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → ((𝑛) = 1o ↔ ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
3433rexbidv 2478 . . . . . . . . . 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 234 . . . . . . 7 ( = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) → ((¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o) ↔ (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o)))
38 subctctexmid.mk . . . . . . . . 9 (𝜑 → ω ∈ Markov)
39 ismkvnex 7147 . . . . . . . . . 10 (ω ∈ Markov → (ω ∈ Markov ↔ ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o)))
4038, 39syl 14 . . . . . . . . 9 (𝜑 → (ω ∈ Markov ↔ ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o)))
4138, 40mpbid 147 . . . . . . . 8 (𝜑 → ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o))
4241adantr 276 . . . . . . 7 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → ∀ ∈ (2o𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (𝑛) = 1o → ∃𝑛 ∈ ω (𝑛) = 1o))
43 1lt2o 6437 . . . . . . . . . . . 12 1o ∈ 2o
4443a1i 9 . . . . . . . . . . 11 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ (1st ‘(𝑔𝑛)) = ∅) → 1o ∈ 2o)
45 0lt2o 6436 . . . . . . . . . . . 12 ∅ ∈ 2o
4645a1i 9 . . . . . . . . . . 11 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ ¬ (1st ‘(𝑔𝑛)) = ∅) → ∅ ∈ 2o)
47 simplr 528 . . . . . . . . . . . . . . 15 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
48 fof 5434 . . . . . . . . . . . . . . 15 (𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
4947, 48syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
50 simpr 110 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
5149, 50ffvelcdmd 5648 . . . . . . . . . . . . 13 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
52 eldju1st 7064 . . . . . . . . . . . . 13 ((𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) → ((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o))
5351, 52syl 14 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → ((1st ‘(𝑔𝑛)) = ∅ ∨ (1st ‘(𝑔𝑛)) = 1o))
54 1n0 6427 . . . . . . . . . . . . . . . 16 1o ≠ ∅
5554neii 2349 . . . . . . . . . . . . . . 15 ¬ 1o = ∅
56 eqeq1 2184 . . . . . . . . . . . . . . 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 3563 . . . . . . . . . 10 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ∈ 2o)
6362fmpttd 5667 . . . . . . . . 9 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)):ω⟶2o)
64 2fveq3 5516 . . . . . . . . . . . . . 14 (𝑤 = 𝑛 → (1st ‘(𝑔𝑤)) = (1st ‘(𝑔𝑛)))
6564eqeq1d 2186 . . . . . . . . . . . . 13 (𝑤 = 𝑛 → ((1st ‘(𝑔𝑤)) = ∅ ↔ (1st ‘(𝑔𝑛)) = ∅))
6665ifbid 3555 . . . . . . . . . . . 12 (𝑤 = 𝑛 → if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
67 eqcom 2179 . . . . . . . . . . . 12 (𝑤 = 𝑛𝑛 = 𝑤)
68 eqcom 2179 . . . . . . . . . . . 12 (if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
6966, 67, 683imtr3i 200 . . . . . . . . . . 11 (𝑛 = 𝑤 → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7069cbvmptv 4096 . . . . . . . . . 10 (𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)) = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7170feq1i 5354 . . . . . . . . 9 ((𝑛 ∈ ω ↦ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅)):ω⟶2o ↔ (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
7263, 71sylib 122 . . . . . . . 8 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
73 2onn 6516 . . . . . . . . . 10 2o ∈ ω
7473elexi 2749 . . . . . . . . 9 2o ∈ V
7574, 2elmap 6671 . . . . . . . 8 ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) ∈ (2o𝑚 ω) ↔ (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)):ω⟶2o)
7672, 75sylibr 134 . . . . . . 7 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) ∈ (2o𝑚 ω))
7737, 42, 76rspcdva 2846 . . . . . 6 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
78 eqid 2177 . . . . . . . . . . . . 13 (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅)) = (𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))
7978, 66, 50, 62fvmptd3 5605 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
8079eqeq1d 2186 . . . . . . . . . . 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 2183 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → 1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅))
84 eqifdc 3568 . . . . . . . . . . . . . . . . . . 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 2177 . . . . . . . . . . . . . . . . . . 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 187 . . . . . . . . . . . . . . . . . . 19 ((((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o) ∨ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)) ↔ ((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o))
9286, 91mpbiran2 941 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝑔𝑛)) = ∅ ∧ 1o = 1o) ∨ (¬ (1st ‘(𝑔𝑛)) = ∅ ∧ 1o = ∅)) ↔ (1st ‘(𝑔𝑛)) = ∅)
9385, 92bitrdi 196 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ (1st ‘(𝑔𝑛)) = ∅))
9493adantr 276 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (1o = if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) ↔ (1st ‘(𝑔𝑛)) = ∅))
9583, 94mpbid 147 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (1st ‘(𝑔𝑛)) = ∅)
96 eldju2ndl 7065 . . . . . . . . . . . . . . 15 (((𝑔𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o) ∧ (1st ‘(𝑔𝑛)) = ∅) → (2nd ‘(𝑔𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
9781, 95, 96syl2anc 411 . . . . . . . . . . . . . 14 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) ∧ if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o) → (2nd ‘(𝑔𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
98 biidd 172 . . . . . . . . . . . . . . 15 (𝑧 = (2nd ‘(𝑔𝑛)) → (𝑦 = {∅} ↔ 𝑦 = {∅}))
9998elrab 2893 . . . . . . . . . . . . . 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 150 . . . . . . . . . 10 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑛 ∈ ω) → (((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o𝑦 = {∅}))
104103rexlimdva 2594 . . . . . . . . 9 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o𝑦 = {∅}))
105 simplr 528 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
106 biidd 172 . . . . . . . . . . . . . 14 (𝑧 = ∅ → (𝑦 = {∅} ↔ 𝑦 = {∅}))
107 peano1 4590 . . . . . . . . . . . . . . 15 ∅ ∈ ω
108107a1i 9 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∅ ∈ ω)
109 simpr 110 . . . . . . . . . . . . . 14 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
110106, 108, 109elrabd 2895 . . . . . . . . . . . . 13 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → ∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
111 djulcl 7044 . . . . . . . . . . . . 13 (∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
112110, 111syl 14 . . . . . . . . . . . 12 (((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o))
113 foelrn 5748 . . . . . . . . . . . 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 5511 . . . . . . . . . . . . . . . 16 ((inl‘∅) = (𝑔𝑛) → (1st ‘(inl‘∅)) = (1st ‘(𝑔𝑛)))
117 1stinl 7067 . . . . . . . . . . . . . . . . 17 (∅ ∈ ω → (1st ‘(inl‘∅)) = ∅)
118107, 117ax-mp 5 . . . . . . . . . . . . . . . 16 (1st ‘(inl‘∅)) = ∅
119116, 118eqtr3di 2225 . . . . . . . . . . . . . . 15 ((inl‘∅) = (𝑔𝑛) → (1st ‘(𝑔𝑛)) = ∅)
120119iftrued 3541 . . . . . . . . . . . . . 14 ((inl‘∅) = (𝑔𝑛) → if((1st ‘(𝑔𝑛)) = ∅, 1o, ∅) = 1o)
121115, 120sylan9eq 2230 . . . . . . . . . . . . 13 (((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) ∧ (inl‘∅) = (𝑔𝑛)) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o)
122121ex 115 . . . . . . . . . . . 12 ((((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) → ((inl‘∅) = (𝑔𝑛) → ((𝑤 ∈ ω ↦ if((1st ‘(𝑔𝑤)) = ∅, 1o, ∅))‘𝑛) = 1o))
123122reximdva 2579 . . . . . . . . . . 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 202 . . . . 5 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
130 df-stab 831 . . . . 5 (STAB 𝑦 = {∅} ↔ (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
131129, 130sylibr 134 . . . 4 ((𝜑𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1o)) → STAB 𝑦 = {∅})
13231, 131exlimddv 1898 . . 3 (𝜑STAB 𝑦 = {∅})
133132adantr 276 . 2 ((𝜑𝑦 ⊆ {∅}) → STAB 𝑦 = {∅})
134133exmid1stab 4205 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 1492  wcel 2148  wral 2455  wrex 2456  {crab 2459  Vcvv 2737  wss 3129  c0 3422  ifcif 3534  {csn 3591  cmpt 4061  EXMIDwem 4191   I cid 4285  ωcom 4586  cres 4625  wf 5208  ontowfo 5210  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  1st c1st 6133  2nd c2nd 6134  1oc1o 6404  2oc2o 6405  𝑚 cmap 6642  cdju 7030  inlcinl 7038  Markovcmarkov 7143
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
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 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-exmid 4192  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-1o 6411  df-2o 6412  df-map 6644  df-dju 7031  df-inl 7040  df-inr 7041  df-markov 7144
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator