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

Theorem exmidfodomrlemr 7201
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 1528 . . . . . . . . 9 Ⅎ𝑓(βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯)
2 nfe1 1496 . . . . . . . . 9 β„²π‘“βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦
31, 2nfim 1572 . . . . . . . 8 Ⅎ𝑓((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦)
43nfal 1576 . . . . . . 7 β„²π‘“βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦)
54nfal 1576 . . . . . 6 β„²π‘“βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦)
6 nfv 1528 . . . . . 6 Ⅎ𝑓 𝑒 βŠ† {βˆ…}
75, 6nfan 1565 . . . . 5 Ⅎ𝑓(βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…})
8 nfv 1528 . . . . 5 Ⅎ𝑓DECID βˆ… ∈ 𝑒
9 simpl 109 . . . . . 6 ((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) β†’ βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦))
10 p0ex 4189 . . . . . . . . . . . 12 {βˆ…} ∈ V
11 ssdomg 6778 . . . . . . . . . . . 12 ({βˆ…} ∈ V β†’ (𝑒 βŠ† {βˆ…} β†’ 𝑒 β‰Ό {βˆ…}))
1210, 11ax-mp 5 . . . . . . . . . . 11 (𝑒 βŠ† {βˆ…} β†’ 𝑒 β‰Ό {βˆ…})
13 df1o2 6430 . . . . . . . . . . 11 1o = {βˆ…}
1412, 13breqtrrdi 4046 . . . . . . . . . 10 (𝑒 βŠ† {βˆ…} β†’ 𝑒 β‰Ό 1o)
15 1onn 6521 . . . . . . . . . . 11 1o ∈ Ο‰
16 domrefg 6767 . . . . . . . . . . 11 (1o ∈ Ο‰ β†’ 1o β‰Ό 1o)
1715, 16ax-mp 5 . . . . . . . . . 10 1o β‰Ό 1o
18 djudom 7092 . . . . . . . . . 10 ((𝑒 β‰Ό 1o ∧ 1o β‰Ό 1o) β†’ (𝑒 βŠ” 1o) β‰Ό (1o βŠ” 1o))
1914, 17, 18sylancl 413 . . . . . . . . 9 (𝑒 βŠ† {βˆ…} β†’ (𝑒 βŠ” 1o) β‰Ό (1o βŠ” 1o))
20 dju1p1e2 7196 . . . . . . . . 9 (1o βŠ” 1o) β‰ˆ 2o
21 domentr 6791 . . . . . . . . 9 (((𝑒 βŠ” 1o) β‰Ό (1o βŠ” 1o) ∧ (1o βŠ” 1o) β‰ˆ 2o) β†’ (𝑒 βŠ” 1o) β‰Ό 2o)
2219, 20, 21sylancl 413 . . . . . . . 8 (𝑒 βŠ† {βˆ…} β†’ (𝑒 βŠ” 1o) β‰Ό 2o)
2322adantl 277 . . . . . . 7 ((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) β†’ (𝑒 βŠ” 1o) β‰Ό 2o)
24 0lt1o 6441 . . . . . . . . 9 βˆ… ∈ 1o
25 djurcl 7051 . . . . . . . . 9 (βˆ… ∈ 1o β†’ (inrβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
2624, 25ax-mp 5 . . . . . . . 8 (inrβ€˜βˆ…) ∈ (𝑒 βŠ” 1o)
27 elex2 2754 . . . . . . . 8 ((inrβ€˜βˆ…) ∈ (𝑒 βŠ” 1o) β†’ βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o))
2826, 27ax-mp 5 . . . . . . 7 βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o)
2923, 28jctil 312 . . . . . 6 ((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) β†’ (βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o) ∧ (𝑒 βŠ” 1o) β‰Ό 2o))
30 vex 2741 . . . . . . . 8 𝑒 ∈ V
31 djuex 7042 . . . . . . . 8 ((𝑒 ∈ V ∧ 1o ∈ Ο‰) β†’ (𝑒 βŠ” 1o) ∈ V)
3230, 15, 31mp2an 426 . . . . . . 7 (𝑒 βŠ” 1o) ∈ V
33 2onn 6522 . . . . . . . 8 2o ∈ Ο‰
34 breq2 4008 . . . . . . . . . . . 12 (π‘₯ = 2o β†’ (𝑦 β‰Ό π‘₯ ↔ 𝑦 β‰Ό 2o))
3534anbi2d 464 . . . . . . . . . . 11 (π‘₯ = 2o β†’ ((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) ↔ (βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o)))
36 foeq2 5436 . . . . . . . . . . . 12 (π‘₯ = 2o β†’ (𝑓:π‘₯–onto→𝑦 ↔ 𝑓:2o–onto→𝑦))
3736exbidv 1825 . . . . . . . . . . 11 (π‘₯ = 2o β†’ (βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦 ↔ βˆƒπ‘“ 𝑓:2o–onto→𝑦))
3835, 37imbi12d 234 . . . . . . . . . 10 (π‘₯ = 2o β†’ (((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ↔ ((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦)))
3938albidv 1824 . . . . . . . . 9 (π‘₯ = 2o β†’ (βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ↔ βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦)))
4039spcgv 2825 . . . . . . . 8 (2o ∈ Ο‰ β†’ (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦)))
4133, 40ax-mp 5 . . . . . . 7 (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦))
42 eleq2 2241 . . . . . . . . . . 11 (𝑦 = (𝑒 βŠ” 1o) β†’ (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑒 βŠ” 1o)))
4342exbidv 1825 . . . . . . . . . 10 (𝑦 = (𝑒 βŠ” 1o) β†’ (βˆƒπ‘§ 𝑧 ∈ 𝑦 ↔ βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o)))
44 breq1 4007 . . . . . . . . . 10 (𝑦 = (𝑒 βŠ” 1o) β†’ (𝑦 β‰Ό 2o ↔ (𝑒 βŠ” 1o) β‰Ό 2o))
4543, 44anbi12d 473 . . . . . . . . 9 (𝑦 = (𝑒 βŠ” 1o) β†’ ((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) ↔ (βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o) ∧ (𝑒 βŠ” 1o) β‰Ό 2o)))
46 foeq3 5437 . . . . . . . . . 10 (𝑦 = (𝑒 βŠ” 1o) β†’ (𝑓:2o–onto→𝑦 ↔ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)))
4746exbidv 1825 . . . . . . . . 9 (𝑦 = (𝑒 βŠ” 1o) β†’ (βˆƒπ‘“ 𝑓:2o–onto→𝑦 ↔ βˆƒπ‘“ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)))
4845, 47imbi12d 234 . . . . . . . 8 (𝑦 = (𝑒 βŠ” 1o) β†’ (((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦) ↔ ((βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o) ∧ (𝑒 βŠ” 1o) β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o))))
4948spcgv 2825 . . . . . . 7 ((𝑒 βŠ” 1o) ∈ V β†’ (βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–onto→𝑦) β†’ ((βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o) ∧ (𝑒 βŠ” 1o) β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o))))
5032, 41, 49mpsyl 65 . . . . . 6 (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ ((βˆƒπ‘§ 𝑧 ∈ (𝑒 βŠ” 1o) ∧ (𝑒 βŠ” 1o) β‰Ό 2o) β†’ βˆƒπ‘“ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)))
519, 29, 50sylc 62 . . . . 5 ((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) β†’ βˆƒπ‘“ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o))
52 simpr 110 . . . . . . . . . 10 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…))
53 fof 5439 . . . . . . . . . . . . 13 (𝑓:2o–ontoβ†’(𝑒 βŠ” 1o) β†’ 𝑓:2o⟢(𝑒 βŠ” 1o))
5453adantl 277 . . . . . . . . . . . 12 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ 𝑓:2o⟢(𝑒 βŠ” 1o))
55 elelsuc 4410 . . . . . . . . . . . . . . 15 (βˆ… ∈ 1o β†’ βˆ… ∈ suc 1o)
5624, 55ax-mp 5 . . . . . . . . . . . . . 14 βˆ… ∈ suc 1o
57 df-2o 6418 . . . . . . . . . . . . . 14 2o = suc 1o
5856, 57eleqtrri 2253 . . . . . . . . . . . . 13 βˆ… ∈ 2o
5958a1i 9 . . . . . . . . . . . 12 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ βˆ… ∈ 2o)
6054, 59ffvelcdmd 5653 . . . . . . . . . . 11 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ (π‘“β€˜βˆ…) ∈ (𝑒 βŠ” 1o))
6160adantr 276 . . . . . . . . . 10 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ (π‘“β€˜βˆ…) ∈ (𝑒 βŠ” 1o))
6252, 61eqeltrrd 2255 . . . . . . . . 9 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
63 0ex 4131 . . . . . . . . . 10 βˆ… ∈ V
64 djulclb 7054 . . . . . . . . . 10 (βˆ… ∈ V β†’ (βˆ… ∈ 𝑒 ↔ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o)))
6563, 64ax-mp 5 . . . . . . . . 9 (βˆ… ∈ 𝑒 ↔ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
6662, 65sylibr 134 . . . . . . . 8 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ βˆ… ∈ 𝑒)
6766orcd 733 . . . . . . 7 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ (βˆ… ∈ 𝑒 ∨ Β¬ βˆ… ∈ 𝑒))
68 df-dc 835 . . . . . . 7 (DECID βˆ… ∈ 𝑒 ↔ (βˆ… ∈ 𝑒 ∨ Β¬ βˆ… ∈ 𝑒))
6967, 68sylibr 134 . . . . . 6 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inlβ€˜βˆ…)) β†’ DECID βˆ… ∈ 𝑒)
70 simpr 110 . . . . . . . . . . 11 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ (π‘“β€˜1o) = (inlβ€˜βˆ…))
7154adantr 276 . . . . . . . . . . . . 13 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ 𝑓:2o⟢(𝑒 βŠ” 1o))
72 1oex 6425 . . . . . . . . . . . . . . . 16 1o ∈ V
7372prid2 3700 . . . . . . . . . . . . . . 15 1o ∈ {βˆ…, 1o}
74 df2o3 6431 . . . . . . . . . . . . . . 15 2o = {βˆ…, 1o}
7573, 74eleqtrri 2253 . . . . . . . . . . . . . 14 1o ∈ 2o
7675a1i 9 . . . . . . . . . . . . 13 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ 1o ∈ 2o)
7771, 76ffvelcdmd 5653 . . . . . . . . . . . 12 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ (π‘“β€˜1o) ∈ (𝑒 βŠ” 1o))
7877adantr 276 . . . . . . . . . . 11 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ (π‘“β€˜1o) ∈ (𝑒 βŠ” 1o))
7970, 78eqeltrrd 2255 . . . . . . . . . 10 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
8079, 65sylibr 134 . . . . . . . . 9 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ βˆ… ∈ 𝑒)
8180orcd 733 . . . . . . . 8 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ (βˆ… ∈ 𝑒 ∨ Β¬ βˆ… ∈ 𝑒))
8281, 68sylibr 134 . . . . . . 7 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inlβ€˜βˆ…)) β†’ DECID βˆ… ∈ 𝑒)
83 simp-4r 542 . . . . . . . . . . . 12 ((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) β†’ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o))
84 djulcl 7050 . . . . . . . . . . . . 13 (βˆ… ∈ 𝑒 β†’ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
8584adantl 277 . . . . . . . . . . . 12 ((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) β†’ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o))
86 foelrn 5754 . . . . . . . . . . . 12 ((𝑓:2o–ontoβ†’(𝑒 βŠ” 1o) ∧ (inlβ€˜βˆ…) ∈ (𝑒 βŠ” 1o)) β†’ βˆƒπ‘€ ∈ 2o (inlβ€˜βˆ…) = (π‘“β€˜π‘€))
8783, 85, 86syl2anc 411 . . . . . . . . . . 11 ((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) β†’ βˆƒπ‘€ ∈ 2o (inlβ€˜βˆ…) = (π‘“β€˜π‘€))
88 simplrr 536 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = βˆ…) β†’ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))
89 simpr 110 . . . . . . . . . . . . . 14 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = βˆ…) β†’ 𝑀 = βˆ…)
9089fveq2d 5520 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = βˆ…) β†’ (π‘“β€˜π‘€) = (π‘“β€˜βˆ…))
91 simp-5r 544 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = βˆ…) β†’ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…))
9288, 90, 913eqtrd 2214 . . . . . . . . . . . 12 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = βˆ…) β†’ (inlβ€˜βˆ…) = (inrβ€˜βˆ…))
93 simplrr 536 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = 1o) β†’ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))
94 simpr 110 . . . . . . . . . . . . . 14 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = 1o) β†’ 𝑀 = 1o)
9594fveq2d 5520 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = 1o) β†’ (π‘“β€˜π‘€) = (π‘“β€˜1o))
96 simp-4r 542 . . . . . . . . . . . . 13 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = 1o) β†’ (π‘“β€˜1o) = (inrβ€˜βˆ…))
9793, 95, 963eqtrd 2214 . . . . . . . . . . . 12 ((((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) ∧ 𝑀 = 1o) β†’ (inlβ€˜βˆ…) = (inrβ€˜βˆ…))
98 elpri 3616 . . . . . . . . . . . . . 14 (𝑀 ∈ {βˆ…, 1o} β†’ (𝑀 = βˆ… ∨ 𝑀 = 1o))
9998, 74eleq2s 2272 . . . . . . . . . . . . 13 (𝑀 ∈ 2o β†’ (𝑀 = βˆ… ∨ 𝑀 = 1o))
10099ad2antrl 490 . . . . . . . . . . . 12 (((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) β†’ (𝑀 = βˆ… ∨ 𝑀 = 1o))
10192, 97, 100mpjaodan 798 . . . . . . . . . . 11 (((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) ∧ (𝑀 ∈ 2o ∧ (inlβ€˜βˆ…) = (π‘“β€˜π‘€))) β†’ (inlβ€˜βˆ…) = (inrβ€˜βˆ…))
10287, 101rexlimddv 2599 . . . . . . . . . 10 ((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) β†’ (inlβ€˜βˆ…) = (inrβ€˜βˆ…))
103 djune 7077 . . . . . . . . . . . . 13 ((βˆ… ∈ V ∧ βˆ… ∈ V) β†’ (inlβ€˜βˆ…) β‰  (inrβ€˜βˆ…))
10463, 63, 103mp2an 426 . . . . . . . . . . . 12 (inlβ€˜βˆ…) β‰  (inrβ€˜βˆ…)
105104neii 2349 . . . . . . . . . . 11 Β¬ (inlβ€˜βˆ…) = (inrβ€˜βˆ…)
106105a1i 9 . . . . . . . . . 10 ((((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) ∧ βˆ… ∈ 𝑒) β†’ Β¬ (inlβ€˜βˆ…) = (inrβ€˜βˆ…))
107102, 106pm2.65da 661 . . . . . . . . 9 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) β†’ Β¬ βˆ… ∈ 𝑒)
108107olcd 734 . . . . . . . 8 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) β†’ (βˆ… ∈ 𝑒 ∨ Β¬ βˆ… ∈ 𝑒))
109108, 68sylibr 134 . . . . . . 7 (((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) ∧ (π‘“β€˜1o) = (inrβ€˜βˆ…)) β†’ DECID βˆ… ∈ 𝑒)
110 simplr 528 . . . . . . . . . 10 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ 𝑒 βŠ† {βˆ…})
111110, 13sseqtrrdi 3205 . . . . . . . . 9 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ 𝑒 βŠ† 1o)
112111adantr 276 . . . . . . . 8 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ 𝑒 βŠ† 1o)
113112, 77exmidfodomrlemeldju 7198 . . . . . . 7 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ ((π‘“β€˜1o) = (inlβ€˜βˆ…) ∨ (π‘“β€˜1o) = (inrβ€˜βˆ…)))
11482, 109, 113mpjaodan 798 . . . . . 6 ((((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) ∧ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)) β†’ DECID βˆ… ∈ 𝑒)
115111, 60exmidfodomrlemeldju 7198 . . . . . 6 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ ((π‘“β€˜βˆ…) = (inlβ€˜βˆ…) ∨ (π‘“β€˜βˆ…) = (inrβ€˜βˆ…)))
11669, 114, 115mpjaodan 798 . . . . 5 (((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) ∧ 𝑓:2o–ontoβ†’(𝑒 βŠ” 1o)) β†’ DECID βˆ… ∈ 𝑒)
1177, 8, 51, 116exlimdd 1872 . . . 4 ((βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) ∧ 𝑒 βŠ† {βˆ…}) β†’ DECID βˆ… ∈ 𝑒)
118117ex 115 . . 3 (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ (𝑒 βŠ† {βˆ…} β†’ DECID βˆ… ∈ 𝑒))
119118alrimiv 1874 . 2 (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ βˆ€π‘’(𝑒 βŠ† {βˆ…} β†’ DECID βˆ… ∈ 𝑒))
120 df-exmid 4196 . 2 (EXMID ↔ βˆ€π‘’(𝑒 βŠ† {βˆ…} β†’ DECID βˆ… ∈ 𝑒))
121119, 120sylibr 134 1 (βˆ€π‘₯βˆ€π‘¦((βˆƒπ‘§ 𝑧 ∈ 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ βˆƒπ‘“ 𝑓:π‘₯–onto→𝑦) β†’ EXMID)
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834  βˆ€wal 1351   = wceq 1353  βˆƒwex 1492   ∈ wcel 2148   β‰  wne 2347  βˆƒwrex 2456  Vcvv 2738   βŠ† wss 3130  βˆ…c0 3423  {csn 3593  {cpr 3594   class class class wbr 4004  EXMIDwem 4195  suc csuc 4366  Ο‰com 4590  βŸΆwf 5213  β€“ontoβ†’wfo 5215  β€˜cfv 5217  1oc1o 6410  2oc2o 6411   β‰ˆ cen 6738   β‰Ό cdom 6739   βŠ” cdju 7036  inlcinl 7044  inrcinr 7045
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-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  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-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-exmid 4196  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-1st 6141  df-2nd 6142  df-1o 6417  df-2o 6418  df-er 6535  df-en 6741  df-dom 6742  df-dju 7037  df-inl 7046  df-inr 7047  df-case 7083
This theorem is referenced by:  exmidfodomr  7203
  Copyright terms: Public domain W3C validator