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

Theorem exmidfodomrlemrALT 6776
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. An alternative proof of exmidfodomrlemr 6775. In particular, this proof uses eldju 6706 instead of djur 6704 and avoids djulclb 6694. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
Assertion
Ref Expression
exmidfodomrlemrALT (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
Distinct variable group:   𝑥,𝑓,𝑦,𝑧

Proof of Theorem exmidfodomrlemrALT
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 3999 . . . . . . . . . . . 12 {∅} ∈ V
11 ssdomg 6449 . . . . . . . . . . . 12 ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
1210, 11ax-mp 7 . . . . . . . . . . 11 (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13 df1o2 6150 . . . . . . . . . . 11 1𝑜 = {∅}
1412, 13syl6breqr 3862 . . . . . . . . . 10 (𝑢 ⊆ {∅} → 𝑢 ≼ 1𝑜)
15 1onn 6233 . . . . . . . . . . 11 1𝑜 ∈ ω
16 domrefg 6438 . . . . . . . . . . 11 (1𝑜 ∈ ω → 1𝑜 ≼ 1𝑜)
1715, 16ax-mp 7 . . . . . . . . . 10 1𝑜 ≼ 1𝑜
18 djudom 6734 . . . . . . . . . 10 ((𝑢 ≼ 1𝑜 ∧ 1𝑜 ≼ 1𝑜) → (𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜))
1914, 17, 18sylancl 404 . . . . . . . . 9 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜))
20 dju1p1e2 6770 . . . . . . . . 9 (1𝑜 ⊔ 1𝑜) ≈ 2𝑜
21 domentr 6462 . . . . . . . . 9 (((𝑢 ⊔ 1𝑜) ≼ (1𝑜 ⊔ 1𝑜) ∧ (1𝑜 ⊔ 1𝑜) ≈ 2𝑜) → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
2219, 20, 21sylancl 404 . . . . . . . 8 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
2322adantl 271 . . . . . . 7 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1𝑜) ≼ 2𝑜)
24 0lt1o 6160 . . . . . . . . 9 ∅ ∈ 1𝑜
25 djurcl 6691 . . . . . . . . 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 6683 . . . . . . . 8 ((𝑢 ∈ V ∧ 1𝑜 ∈ ω) → (𝑢 ⊔ 1𝑜) ∈ V)
3230, 15, 31mp2an 417 . . . . . . 7 (𝑢 ⊔ 1𝑜) ∈ V
33 2onn 6234 . . . . . . . 8 2𝑜 ∈ ω
34 breq2 3826 . . . . . . . . . . . 12 (𝑥 = 2𝑜 → (𝑦𝑥𝑦 ≼ 2𝑜))
3534anbi2d 452 . . . . . . . . . . 11 (𝑥 = 2𝑜 → ((∃𝑧 𝑧𝑦𝑦𝑥) ↔ (∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜)))
36 foeq2 5195 . . . . . . . . . . . 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 3825 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1𝑜) → (𝑦 ≼ 2𝑜 ↔ (𝑢 ⊔ 1𝑜) ≼ 2𝑜))
4543, 44anbi12d 457 . . . . . . . . 9 (𝑦 = (𝑢 ⊔ 1𝑜) → ((∃𝑧 𝑧𝑦𝑦 ≼ 2𝑜) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1𝑜) ∧ (𝑢 ⊔ 1𝑜) ≼ 2𝑜)))
46 foeq3 5196 . . . . . . . . . 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 simprl 498 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
5352orcd 685 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
54 df-dc 779 . . . . . . 7 (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
5553, 54sylibr 132 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
56 simprl 498 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1𝑜) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
5756orcd 685 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1𝑜) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
5857, 54sylibr 132 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1𝑜) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
59 simp-4r 509 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜))
60 djulcl 6690 . . . . . . . . . . . . 13 (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
6160adantl 271 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1𝑜))
62 foelrn 5494 . . . . . . . . . . . 12 ((𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1𝑜)) → ∃𝑤 ∈ 2𝑜 (inl‘∅) = (𝑓𝑤))
6359, 61, 62syl2anc 403 . . . . . . . . . . 11 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2𝑜 (inl‘∅) = (𝑓𝑤))
64 simprr 499 . . . . . . . . . . . . . . 15 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → (inl‘∅) = (𝑓𝑤))
65 fvres 5294 . . . . . . . . . . . . . . . . 17 (∅ ∈ 𝑢 → ((inl ↾ 𝑢)‘∅) = (inl‘∅))
6665eqeq1d 2093 . . . . . . . . . . . . . . . 16 (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = (𝑓𝑤) ↔ (inl‘∅) = (𝑓𝑤)))
6766ad2antlr 473 . . . . . . . . . . . . . . 15 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → (((inl ↾ 𝑢)‘∅) = (𝑓𝑤) ↔ (inl‘∅) = (𝑓𝑤)))
6864, 67mpbird 165 . . . . . . . . . . . . . 14 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
6968adantr 270 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
70 simpr 108 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
7170fveq2d 5274 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓𝑤) = (𝑓‘∅))
72 simp-5r 511 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅))
7369, 71, 723eqtrd 2121 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
7468adantr 270 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
75 simpr 108 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → 𝑤 = 1𝑜)
7675fveq2d 5274 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (𝑓𝑤) = (𝑓‘1𝑜))
77 simp-4r 509 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅))
7874, 76, 773eqtrd 2121 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1𝑜) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
79 elpri 3454 . . . . . . . . . . . . . 14 (𝑤 ∈ {∅, 1𝑜} → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
80 df2o3 6151 . . . . . . . . . . . . . 14 2𝑜 = {∅, 1𝑜}
8179, 80eleq2s 2179 . . . . . . . . . . . . 13 (𝑤 ∈ 2𝑜 → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
8281ad2antrl 474 . . . . . . . . . . . 12 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1𝑜))
8373, 78, 82mpjaodan 745 . . . . . . . . . . 11 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2𝑜 ∧ (inl‘∅) = (𝑓𝑤))) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
8463, 83rexlimddv 2489 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
85 0ex 3943 . . . . . . . . . . . . . 14 ∅ ∈ V
86 djune 6716 . . . . . . . . . . . . . 14 ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
8785, 85, 86mp2an 417 . . . . . . . . . . . . 13 (inl‘∅) ≠ (inr‘∅)
8887neii 2253 . . . . . . . . . . . 12 ¬ (inl‘∅) = (inr‘∅)
89 fvres 5294 . . . . . . . . . . . . . . 15 (∅ ∈ 1𝑜 → ((inr ↾ 1𝑜)‘∅) = (inr‘∅))
9024, 89ax-mp 7 . . . . . . . . . . . . . 14 ((inr ↾ 1𝑜)‘∅) = (inr‘∅)
9190a1i 9 . . . . . . . . . . . . 13 (∅ ∈ 𝑢 → ((inr ↾ 1𝑜)‘∅) = (inr‘∅))
9265, 91eqeq12d 2099 . . . . . . . . . . . 12 (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅) ↔ (inl‘∅) = (inr‘∅)))
9388, 92mtbiri 633 . . . . . . . . . . 11 (∅ ∈ 𝑢 → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
9493adantl 271 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) ∧ ∅ ∈ 𝑢) → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1𝑜)‘∅))
9584, 94pm2.65da 620 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) → ¬ ∅ ∈ 𝑢)
9695olcd 686 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
9796, 54sylibr 132 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) ∧ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)) → DECID ∅ ∈ 𝑢)
98 simplr 497 . . . . . . . . . 10 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑢 ⊆ {∅})
9998, 13syl6sseqr 3062 . . . . . . . . 9 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑢 ⊆ 1𝑜)
10099adantr 270 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → 𝑢 ⊆ 1𝑜)
101 fof 5198 . . . . . . . . . . 11 (𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
102101adantl 271 . . . . . . . . . 10 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
103102adantr 270 . . . . . . . . 9 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → 𝑓:2𝑜⟶(𝑢 ⊔ 1𝑜))
104 1oex 6145 . . . . . . . . . . . 12 1𝑜 ∈ V
105104prid2 3534 . . . . . . . . . . 11 1𝑜 ∈ {∅, 1𝑜}
106105, 80eleqtrri 2160 . . . . . . . . . 10 1𝑜 ∈ 2𝑜
107106a1i 9 . . . . . . . . 9 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → 1𝑜 ∈ 2𝑜)
108103, 107ffvelrnd 5400 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → (𝑓‘1𝑜) ∈ (𝑢 ⊔ 1𝑜))
109100, 108exmidfodomrlemreseldju 6773 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → ((∅ ∈ 𝑢 ∧ (𝑓‘1𝑜) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘1𝑜) = ((inr ↾ 1𝑜)‘∅)))
11058, 97, 109mpjaodan 745 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) ∧ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)) → DECID ∅ ∈ 𝑢)
111 elelsuc 4212 . . . . . . . . . . 11 (∅ ∈ 1𝑜 → ∅ ∈ suc 1𝑜)
11224, 111ax-mp 7 . . . . . . . . . 10 ∅ ∈ suc 1𝑜
113 df-2o 6138 . . . . . . . . . 10 2𝑜 = suc 1𝑜
114112, 113eleqtrri 2160 . . . . . . . . 9 ∅ ∈ 2𝑜
115114a1i 9 . . . . . . . 8 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → ∅ ∈ 2𝑜)
116102, 115ffvelrnd 5400 . . . . . . 7 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1𝑜))
11799, 116exmidfodomrlemreseldju 6773 . . . . . 6 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → ((∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘∅) = ((inr ↾ 1𝑜)‘∅)))
11855, 110, 117mpjaodan 745 . . . . 5 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2𝑜onto→(𝑢 ⊔ 1𝑜)) → DECID ∅ ∈ 𝑢)
1197, 8, 51, 118exlimdd 1797 . . . 4 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
120119ex 113 . . 3 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121120alrimiv 1799 . 2 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
122 df-exmid 4006 . 2 (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
123121, 122sylibr 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 3822  EXMIDwem 4005  suc csuc 4168  ωcom 4380  cres 4415  wf 4979  ontowfo 4981  cfv 4983  1𝑜c1o 6130  2𝑜c2o 6131  cen 6409  cdom 6410  cdju 6677  inlcinl 6684  inrcinr 6685
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 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378
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 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-exmid 4006  df-id 4096  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-1st 5870  df-2nd 5871  df-1o 6137  df-2o 6138  df-er 6246  df-en 6412  df-dom 6413  df-dju 6678  df-inl 6686  df-inr 6687  df-case 6722
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator