ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmidfodomrlemr GIF version

Theorem exmidfodomrlemr 6772
Description: The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
Assertion
Ref Expression
exmidfodomrlemr (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
Distinct variable group:   𝑥,𝑓,𝑦,𝑧

Proof of Theorem exmidfodomrlemr
Dummy variables 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1464 . . . . . . . . 9 𝑓(∃𝑧 𝑧𝑦𝑦𝑥)
2 nfe1 1428 . . . . . . . . 9 𝑓𝑓 𝑓:𝑥onto𝑦
31, 2nfim 1507 . . . . . . . 8 𝑓((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
43nfal 1511 . . . . . . 7 𝑓𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
54nfal 1511 . . . . . 6 𝑓𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
6 nfv 1464 . . . . . 6 𝑓 𝑢 ⊆ {∅}
75, 6nfan 1500 . . . . 5 𝑓(∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅})
8 nfv 1464 . . . . 5 𝑓DECID ∅ ∈ 𝑢
9 simpl 107 . . . . . 6 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦))
10 p0ex 3997 . . . . . . . . . . . 12 {∅} ∈ V
11 ssdomg 6447 . . . . . . . . . . . 12 ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
1210, 11ax-mp 7 . . . . . . . . . . 11 (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13 df1o2 6148 . . . . . . . . . . 11 1𝑜 = {∅}
1412, 13syl6breqr 3860 . . . . . . . . . 10 (𝑢 ⊆ {∅} → 𝑢 ≼ 1𝑜)
15 1onn 6231 . . . . . . . . . . 11 1𝑜 ∈ ω
16 domrefg 6436 . . . . . . . . . . 11 (1𝑜 ∈ ω → 1𝑜 ≼ 1𝑜)
1715, 16ax-mp 7 . . . . . . . . . 10 1𝑜 ≼ 1𝑜
18 djudom 6731 . . . . . . . . . 10 ((𝑢 ≼ 1𝑜 ∧ 1𝑜 ≼ 1𝑜) → (𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜))
1914, 17, 18sylancl 404 . . . . . . . . 9 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜))
20 dju1p1e2 6767 . . . . . . . . 9 (1𝑜 ⊔ 1𝑜) ≈ 2𝑜
21 domentr 6460 . . . . . . . . 9 (((𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜) ∧ (1𝑜 ⊔ 1𝑜) ≈ 2𝑜) → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
2219, 20, 21sylancl 404 . . . . . . . 8 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
2322adantl 271 . . . . . . 7 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
24 0lt1o 6158 . . . . . . . . 9 ∅ ∈ 1𝑜
25 djurcl 6688 . . . . . . . . 9 (∅ ∈ 1𝑜 → (inr‘∅) ∈ (𝑢 ⊔ 1𝑜))
2624, 25ax-mp 7 . . . . . . . 8 (inr‘∅) ∈ (𝑢 ⊔ 1𝑜)
27 elex2 2629 . . . . . . . 8 ((inr‘∅) ∈ (𝑢 ⊔ 1𝑜) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜))
2826, 27ax-mp 7 . . . . . . 7 𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜)
2923, 28jctil 305 . . . . . 6 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜))
30 vex 2618 . . . . . . . 8 𝑢 ∈ V
31 djuex 6680 . . . . . . . 8 ((𝑢 ∈ V ∧ 1𝑜 ∈ ω) → (𝑢 ⊔ 1𝑜) ∈ V)
3230, 15, 31mp2an 417 . . . . . . 7 (𝑢 ⊔ 1𝑜) ∈ V
33 2onn 6232 . . . . . . . 8 2𝑜 ∈ ω
34 breq2 3824 . . . . . . . . . . . 12 (𝑥 = 2𝑜 → (𝑦𝑥𝑦 ≼ 2𝑜))
3534anbi2d 452 . . . . . . . . . . 11 (𝑥 = 2𝑜 → ((∃𝑧 𝑧𝑦𝑦𝑥) ↔ (∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜)))
36 foeq2 5193 . . . . . . . . . . . 12 (𝑥 = 2𝑜 → (𝑓:𝑥onto𝑦𝑓:2𝑜onto𝑦))
3736exbidv 1750 . . . . . . . . . . 11 (𝑥 = 2𝑜 → (∃𝑓 𝑓:𝑥onto𝑦 ↔ ∃𝑓 𝑓:2𝑜onto𝑦))
3835, 37imbi12d 232 . . . . . . . . . 10 (𝑥 = 2𝑜 → (((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ↔ ((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦)))
3938albidv 1749 . . . . . . . . 9 (𝑥 = 2𝑜 → (∀𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ↔ ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦)))
4039spcgv 2699 . . . . . . . 8 (2𝑜 ∈ ω → (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦)))
4133, 40ax-mp 7 . . . . . . 7 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦))
42 eleq2 2148 . . . . . . . . . . 11 (𝑦 = (𝑢 ⊔ 1𝑜) → (𝑧𝑦𝑧 ∈ (𝑢 ⊔ 1𝑜)))
4342exbidv 1750 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1𝑜) → (∃𝑧 𝑧𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜)))
44 breq1 3823 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1𝑜) → (𝑦 ≼ 2𝑜 ↔ (𝑢 ⊔ 1𝑜) ≼ 2𝑜))
4543, 44anbi12d 457 . . . . . . . . 9 (𝑦 = (𝑢 ⊔ 1𝑜) → ((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜)))
46 foeq3 5194 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1𝑜) → (𝑓:2𝑜onto𝑦𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)))
4746exbidv 1750 . . . . . . . . 9 (𝑦 = (𝑢 ⊔ 1𝑜) → (∃𝑓 𝑓:2𝑜onto𝑦 ↔ ∃𝑓 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)))
4845, 47imbi12d 232 . . . . . . . 8 (𝑦 = (𝑢 ⊔ 1𝑜) → (((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜))))
4948spcgv 2699 . . . . . . 7 ((𝑢 ⊔ 1𝑜) ∈ V → (∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜))))
5032, 41, 49mpsyl 64 . . . . . 6 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜) → ∃𝑓 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)))
519, 29, 50sylc 61 . . . . 5 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → ∃𝑓 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜))
52 simpr 108 . . . . . . . . . 10 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) = (inl‘∅))
53 fof 5196 . . . . . . . . . . . . 13 (𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
5453adantl 271 . . . . . . . . . . . 12 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
55 elelsuc 4210 . . . . . . . . . . . . . . 15 (∅ ∈ 1𝑜 → ∅ ∈ suc 1𝑜)
5624, 55ax-mp 7 . . . . . . . . . . . . . 14 ∅ ∈ suc 1𝑜
57 df-2o 6136 . . . . . . . . . . . . . 14 2𝑜 = suc 1𝑜
5856, 57eleqtrri 2160 . . . . . . . . . . . . 13 ∅ ∈ 2𝑜
5958a1i 9 . . . . . . . . . . . 12 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → ∅ ∈ 2𝑜)
6054, 59ffvelrnd 5398 . . . . . . . . . . 11 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1𝑜))
6160adantr 270 . . . . . . . . . 10 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1𝑜))
6252, 61eqeltrrd 2162 . . . . . . . . 9 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
63 0ex 3941 . . . . . . . . . 10 ∅ ∈ V
64 djulclb 6691 . . . . . . . . . 10 (∅ ∈ V → (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1𝑜)))
6563, 64ax-mp 7 . . . . . . . . 9 (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
6662, 65sylibr 132 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → ∅ ∈ 𝑢)
6766orcd 685 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
68 df-dc 779 . . . . . . 7 (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
6967, 68sylibr 132 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
70 simpr 108 . . . . . . . . . . 11 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → (𝑓‘1𝑜) = (inl‘∅))
7154adantr 270 . . . . . . . . . . . . 13 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
72 1oex 6143 . . . . . . . . . . . . . . . 16 1𝑜 ∈ V
7372prid2 3532 . . . . . . . . . . . . . . 15 1𝑜 ∈ {∅, 1𝑜}
74 df2o3 6149 . . . . . . . . . . . . . . 15 2𝑜 = {∅, 1𝑜}
7573, 74eleqtrri 2160 . . . . . . . . . . . . . 14 1𝑜 ∈ 2𝑜
7675a1i 9 . . . . . . . . . . . . 13 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → 1𝑜 ∈ 2𝑜)
7771, 76ffvelrnd 5398 . . . . . . . . . . . 12 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → (𝑓‘1𝑜) ∈ (𝑢 ⊔ 1𝑜))
7877adantr 270 . . . . . . . . . . 11 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → (𝑓‘1𝑜) ∈ (𝑢 ⊔ 1𝑜))
7970, 78eqeltrrd 2162 . . . . . . . . . 10 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
8079, 65sylibr 132 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → ∅ ∈ 𝑢)
8180orcd 685 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
8281, 68sylibr 132 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
83 simp-4r 509 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜))
84 djulcl 6687 . . . . . . . . . . . . 13 (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
8584adantl 271 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
86 foelrn 5492 . . . . . . . . . . . 12 ((𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1𝑜)) → ∃𝑤 ∈ 2𝑜 (inl‘∅) = (𝑓𝑤))
8783, 85, 86syl2anc 403 . . . . . . . . . . 11 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2𝑜 (inl‘∅) = (𝑓𝑤))
88 simplrr 503 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (𝑓𝑤))
89 simpr 108 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
9089fveq2d 5272 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓𝑤) = (𝑓‘∅))
91 simp-5r 511 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = (inr‘∅))
9288, 90, 913eqtrd 2121 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (inr‘∅))
93 simplrr 503 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (inl‘∅) = (𝑓𝑤))
94 simpr 108 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → 𝑤 = 1𝑜)
9594fveq2d 5272 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (𝑓𝑤) = (𝑓‘1𝑜))
96 simp-4r 509 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (𝑓‘1𝑜) = (inr‘∅))
9793, 95, 963eqtrd 2121 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (inl‘∅) = (inr‘∅))
98 elpri 3454 . . . . . . . . . . . . . 14 (𝑤 ∈ {∅, 1𝑜} → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
9998, 74eleq2s 2179 . . . . . . . . . . . . 13 (𝑤 ∈ 2𝑜 → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
10099ad2antrl 474 . . . . . . . . . . . 12 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
10192, 97, 100mpjaodan 745 . . . . . . . . . . 11 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → (inl‘∅) = (inr‘∅))
10287, 101rexlimddv 2489 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103 djune 6713 . . . . . . . . . . . . 13 ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
10463, 63, 103mp2an 417 . . . . . . . . . . . 12 (inl‘∅) ≠ (inr‘∅)
105104neii 2253 . . . . . . . . . . 11 ¬ (inl‘∅) = (inr‘∅)
106105a1i 9 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ¬ (inl‘∅) = (inr‘∅))
107102, 106pm2.65da 620 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) → ¬ ∅ ∈ 𝑢)
108107olcd 686 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
109108, 68sylibr 132 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1𝑜) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
110 simplr 497 . . . . . . . . . 10 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑢 ⊆ {∅})
111110, 13syl6sseqr 3062 . . . . . . . . 9 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑢 ⊆ 1𝑜)
112111adantr 270 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1𝑜)
113112, 77exmidfodomrlemeldju 6769 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → ((𝑓‘1𝑜) = (inl‘∅) ∨ (𝑓‘1𝑜) = (inr‘∅)))
11482, 109, 113mpjaodan 745 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
115111, 60exmidfodomrlemeldju 6769 . . . . . 6 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → ((𝑓‘∅) = (inl‘∅) ∨ (𝑓‘∅) = (inr‘∅)))
11669, 114, 115mpjaodan 745 . . . . 5 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → DECID ∅ ∈ 𝑢)
1177, 8, 51, 116exlimdd 1797 . . . 4 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
118117ex 113 . . 3 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
119118alrimiv 1799 . 2 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
120 df-exmid 4004 . 2 (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121119, 120sylibr 132 1 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  DECID wdc 778  wal 1285   = wceq 1287  wex 1424  wcel 1436  wne 2251  wrex 2356  Vcvv 2615  wss 2988  c0 3275  {csn 3431  {cpr 3432   class class class wbr 3820  EXMIDwem 4003  suc csuc 4166  ωcom 4378  wf 4977  ontowfo 4979  cfv 4981  1𝑜c1o 6128  2𝑜c2o 6129  cen 6407  cdom 6408  cdju 6674  inlcinl 6681  inrcinr 6682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3929  ax-sep 3932  ax-nul 3940  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-iinf 4376
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-iun 3715  df-br 3821  df-opab 3875  df-mpt 3876  df-tr 3912  df-exmid 4004  df-id 4094  df-iord 4167  df-on 4169  df-suc 4172  df-iom 4379  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-res 4423  df-ima 4424  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-f1 4986  df-fo 4987  df-f1o 4988  df-fv 4989  df-1st 5868  df-2nd 5869  df-1o 6135  df-2o 6136  df-er 6244  df-en 6410  df-dom 6411  df-dju 6675  df-inl 6683  df-inr 6684  df-case 6719
This theorem is referenced by:  exmidfodomr  6774
  Copyright terms: Public domain W3C validator