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

Theorem exmidfodomrlemrALT 7232
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 7231. In particular, this proof uses eldju 7097 instead of djur 7098 and avoids djulclb 7084. (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 1539 . . . . . . . . 9 𝑓(∃𝑧 𝑧𝑦𝑦𝑥)
2 nfe1 1507 . . . . . . . . 9 𝑓𝑓 𝑓:𝑥onto𝑦
31, 2nfim 1583 . . . . . . . 8 𝑓((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
43nfal 1587 . . . . . . 7 𝑓𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
54nfal 1587 . . . . . 6 𝑓𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦)
6 nfv 1539 . . . . . 6 𝑓 𝑢 ⊆ {∅}
75, 6nfan 1576 . . . . 5 𝑓(∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅})
8 nfv 1539 . . . . 5 𝑓DECID ∅ ∈ 𝑢
9 simpl 109 . . . . . 6 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦))
10 p0ex 4206 . . . . . . . . . . . 12 {∅} ∈ V
11 ssdomg 6804 . . . . . . . . . . . 12 ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
1210, 11ax-mp 5 . . . . . . . . . . 11 (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13 df1o2 6454 . . . . . . . . . . 11 1o = {∅}
1412, 13breqtrrdi 4060 . . . . . . . . . 10 (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15 1onn 6545 . . . . . . . . . . 11 1o ∈ ω
16 domrefg 6793 . . . . . . . . . . 11 (1o ∈ ω → 1o ≼ 1o)
1715, 16ax-mp 5 . . . . . . . . . 10 1o ≼ 1o
18 djudom 7122 . . . . . . . . . 10 ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
1914, 17, 18sylancl 413 . . . . . . . . 9 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20 dju1p1e2 7226 . . . . . . . . 9 (1o ⊔ 1o) ≈ 2o
21 domentr 6817 . . . . . . . . 9 (((𝑢 ⊔ 1o) ≼ (1o ⊔ 1o) ∧ (1o ⊔ 1o) ≈ 2o) → (𝑢 ⊔ 1o) ≼ 2o)
2219, 20, 21sylancl 413 . . . . . . . 8 (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ 2o)
2322adantl 277 . . . . . . 7 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1o) ≼ 2o)
24 0lt1o 6465 . . . . . . . . 9 ∅ ∈ 1o
25 djurcl 7081 . . . . . . . . 9 (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
2624, 25ax-mp 5 . . . . . . . 8 (inr‘∅) ∈ (𝑢 ⊔ 1o)
27 elex2 2768 . . . . . . . 8 ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
2826, 27ax-mp 5 . . . . . . 7 𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
2923, 28jctil 312 . . . . . 6 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30 vex 2755 . . . . . . . 8 𝑢 ∈ V
31 djuex 7072 . . . . . . . 8 ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
3230, 15, 31mp2an 426 . . . . . . 7 (𝑢 ⊔ 1o) ∈ V
33 2onn 6546 . . . . . . . 8 2o ∈ ω
34 breq2 4022 . . . . . . . . . . . 12 (𝑥 = 2o → (𝑦𝑥𝑦 ≼ 2o))
3534anbi2d 464 . . . . . . . . . . 11 (𝑥 = 2o → ((∃𝑧 𝑧𝑦𝑦𝑥) ↔ (∃𝑧 𝑧𝑦𝑦 ≼ 2o)))
36 foeq2 5454 . . . . . . . . . . . 12 (𝑥 = 2o → (𝑓:𝑥onto𝑦𝑓:2oonto𝑦))
3736exbidv 1836 . . . . . . . . . . 11 (𝑥 = 2o → (∃𝑓 𝑓:𝑥onto𝑦 ↔ ∃𝑓 𝑓:2oonto𝑦))
3835, 37imbi12d 234 . . . . . . . . . 10 (𝑥 = 2o → (((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ↔ ((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦)))
3938albidv 1835 . . . . . . . . 9 (𝑥 = 2o → (∀𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ↔ ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦)))
4039spcgv 2839 . . . . . . . 8 (2o ∈ ω → (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦)))
4133, 40ax-mp 5 . . . . . . 7 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦))
42 eleq2 2253 . . . . . . . . . . 11 (𝑦 = (𝑢 ⊔ 1o) → (𝑧𝑦𝑧 ∈ (𝑢 ⊔ 1o)))
4342exbidv 1836 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44 breq1 4021 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
4543, 44anbi12d 473 . . . . . . . . 9 (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧𝑦𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46 foeq3 5455 . . . . . . . . . 10 (𝑦 = (𝑢 ⊔ 1o) → (𝑓:2oonto𝑦𝑓:2oonto→(𝑢 ⊔ 1o)))
4746exbidv 1836 . . . . . . . . 9 (𝑦 = (𝑢 ⊔ 1o) → (∃𝑓 𝑓:2oonto𝑦 ↔ ∃𝑓 𝑓:2oonto→(𝑢 ⊔ 1o)))
4845, 47imbi12d 234 . . . . . . . 8 (𝑦 = (𝑢 ⊔ 1o) → (((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2oonto→(𝑢 ⊔ 1o))))
4948spcgv 2839 . . . . . . 7 ((𝑢 ⊔ 1o) ∈ V → (∀𝑦((∃𝑧 𝑧𝑦𝑦 ≼ 2o) → ∃𝑓 𝑓:2oonto𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2oonto→(𝑢 ⊔ 1o))))
5032, 41, 49mpsyl 65 . . . . . 6 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2oonto→(𝑢 ⊔ 1o)))
519, 29, 50sylc 62 . . . . 5 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → ∃𝑓 𝑓:2oonto→(𝑢 ⊔ 1o))
52 simprl 529 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
5352orcd 734 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
54 df-dc 836 . . . . . . 7 (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
5553, 54sylibr 134 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
56 simprl 529 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
5756orcd 734 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
5857, 54sylibr 134 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
59 simp-4r 542 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2oonto→(𝑢 ⊔ 1o))
60 djulcl 7080 . . . . . . . . . . . . 13 (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
6160adantl 277 . . . . . . . . . . . 12 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
62 foelrn 5774 . . . . . . . . . . . 12 ((𝑓:2oonto→(𝑢 ⊔ 1o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1o)) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓𝑤))
6359, 61, 62syl2anc 411 . . . . . . . . . . 11 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓𝑤))
64 simprr 531 . . . . . . . . . . . . . . 15 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) → (inl‘∅) = (𝑓𝑤))
65 fvres 5558 . . . . . . . . . . . . . . . . 17 (∅ ∈ 𝑢 → ((inl ↾ 𝑢)‘∅) = (inl‘∅))
6665eqeq1d 2198 . . . . . . . . . . . . . . . 16 (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = (𝑓𝑤) ↔ (inl‘∅) = (𝑓𝑤)))
6766ad2antlr 489 . . . . . . . . . . . . . . 15 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) → (((inl ↾ 𝑢)‘∅) = (𝑓𝑤) ↔ (inl‘∅) = (𝑓𝑤)))
6864, 67mpbird 167 . . . . . . . . . . . . . 14 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
6968adantr 276 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
70 simpr 110 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
7170fveq2d 5538 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓𝑤) = (𝑓‘∅))
72 simp-5r 544 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = ((inr ↾ 1o)‘∅))
7369, 71, 723eqtrd 2226 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
7468adantr 276 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1o) → ((inl ↾ 𝑢)‘∅) = (𝑓𝑤))
75 simpr 110 . . . . . . . . . . . . . 14 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1o) → 𝑤 = 1o)
7675fveq2d 5538 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1o) → (𝑓𝑤) = (𝑓‘1o))
77 simp-4r 542 . . . . . . . . . . . . 13 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1o) → (𝑓‘1o) = ((inr ↾ 1o)‘∅))
7874, 76, 773eqtrd 2226 . . . . . . . . . . . 12 ((((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) ∧ 𝑤 = 1o) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
79 elpri 3630 . . . . . . . . . . . . . 14 (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
80 df2o3 6455 . . . . . . . . . . . . . 14 2o = {∅, 1o}
8179, 80eleq2s 2284 . . . . . . . . . . . . 13 (𝑤 ∈ 2o → (𝑤 = ∅ ∨ 𝑤 = 1o))
8281ad2antrl 490 . . . . . . . . . . . 12 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1o))
8373, 78, 82mpjaodan 799 . . . . . . . . . . 11 (((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓𝑤))) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
8463, 83rexlimddv 2612 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
85 0ex 4145 . . . . . . . . . . . . . 14 ∅ ∈ V
86 djune 7107 . . . . . . . . . . . . . 14 ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
8785, 85, 86mp2an 426 . . . . . . . . . . . . 13 (inl‘∅) ≠ (inr‘∅)
8887neii 2362 . . . . . . . . . . . 12 ¬ (inl‘∅) = (inr‘∅)
89 fvres 5558 . . . . . . . . . . . . . . 15 (∅ ∈ 1o → ((inr ↾ 1o)‘∅) = (inr‘∅))
9024, 89ax-mp 5 . . . . . . . . . . . . . 14 ((inr ↾ 1o)‘∅) = (inr‘∅)
9190a1i 9 . . . . . . . . . . . . 13 (∅ ∈ 𝑢 → ((inr ↾ 1o)‘∅) = (inr‘∅))
9265, 91eqeq12d 2204 . . . . . . . . . . . 12 (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅) ↔ (inl‘∅) = (inr‘∅)))
9388, 92mtbiri 676 . . . . . . . . . . 11 (∅ ∈ 𝑢 → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
9493adantl 277 . . . . . . . . . 10 ((((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
9584, 94pm2.65da 662 . . . . . . . . 9 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → ¬ ∅ ∈ 𝑢)
9695olcd 735 . . . . . . . 8 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
9796, 54sylibr 134 . . . . . . 7 (((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → DECID ∅ ∈ 𝑢)
98 simplr 528 . . . . . . . . . 10 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ {∅})
9998, 13sseqtrrdi 3219 . . . . . . . . 9 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
10099adantr 276 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 𝑢 ⊆ 1o)
101 fof 5457 . . . . . . . . . . 11 (𝑓:2oonto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
102101adantl 277 . . . . . . . . . 10 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
103102adantr 276 . . . . . . . . 9 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
104 1oex 6449 . . . . . . . . . . . 12 1o ∈ V
105104prid2 3714 . . . . . . . . . . 11 1o ∈ {∅, 1o}
106105, 80eleqtrri 2265 . . . . . . . . . 10 1o ∈ 2o
107106a1i 9 . . . . . . . . 9 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 1o ∈ 2o)
108103, 107ffvelcdmd 5673 . . . . . . . 8 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
109100, 108exmidfodomrlemreseldju 7229 . . . . . . 7 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → ((∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘1o) = ((inr ↾ 1o)‘∅)))
11058, 97, 109mpjaodan 799 . . . . . 6 ((((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → DECID ∅ ∈ 𝑢)
111 elelsuc 4427 . . . . . . . . . . 11 (∅ ∈ 1o → ∅ ∈ suc 1o)
11224, 111ax-mp 5 . . . . . . . . . 10 ∅ ∈ suc 1o
113 df-2o 6442 . . . . . . . . . 10 2o = suc 1o
114112, 113eleqtrri 2265 . . . . . . . . 9 ∅ ∈ 2o
115114a1i 9 . . . . . . . 8 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
116102, 115ffvelcdmd 5673 . . . . . . 7 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
11799, 116exmidfodomrlemreseldju 7229 . . . . . 6 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → ((∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘∅) = ((inr ↾ 1o)‘∅)))
11855, 110, 117mpjaodan 799 . . . . 5 (((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2oonto→(𝑢 ⊔ 1o)) → DECID ∅ ∈ 𝑢)
1197, 8, 51, 118exlimdd 1883 . . . 4 ((∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
120119ex 115 . . 3 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121120alrimiv 1885 . 2 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
122 df-exmid 4213 . 2 (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
123121, 122sylibr 134 1 (∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  wal 1362   = wceq 1364  wex 1503  wcel 2160  wne 2360  wrex 2469  Vcvv 2752  wss 3144  c0 3437  {csn 3607  {cpr 3608   class class class wbr 4018  EXMIDwem 4212  suc csuc 4383  ωcom 4607  cres 4646  wf 5231  ontowfo 5233  cfv 5235  1oc1o 6434  2oc2o 6435  cen 6764  cdom 6765  cdju 7066  inlcinl 7074  inrcinr 7075
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-exmid 4213  df-id 4311  df-iord 4384  df-on 4386  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-1st 6165  df-2nd 6166  df-1o 6441  df-2o 6442  df-er 6559  df-en 6767  df-dom 6768  df-dju 7067  df-inl 7076  df-inr 7077  df-case 7113
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator