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

Theorem exmidsbthrlem 14740
Description: Lemma for exmidsbthr 14741. (Contributed by Jim Kingdon, 11-Aug-2022.)
Hypothesis
Ref Expression
exmidsbthrlem.s 𝑆 = (𝑝 ∈ β„•βˆž ↦ (𝑖 ∈ Ο‰ ↦ if(𝑖 = βˆ…, 1o, (π‘β€˜βˆͺ 𝑖))))
Assertion
Ref Expression
exmidsbthrlem (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ EXMID)
Distinct variable groups:   𝑆,𝑖   𝑖,𝑝   π‘₯,𝑦
Allowed substitution hints:   𝑆(π‘₯,𝑦,𝑝)

Proof of Theorem exmidsbthrlem
Dummy variables π‘Ž 𝑏 π‘˜ 𝑧 𝑓 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 109 . . . . . . 7 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦))
2 nninfex 7119 . . . . . . . . . 10 β„•βˆž ∈ V
3 fconstmpt 4673 . . . . . . . . . . . . . . 15 (Ο‰ Γ— {βˆ…}) = (𝑖 ∈ Ο‰ ↦ βˆ…)
4 0nninf 14723 . . . . . . . . . . . . . . 15 (Ο‰ Γ— {βˆ…}) ∈ β„•βˆž
53, 4eqeltrri 2251 . . . . . . . . . . . . . 14 (𝑖 ∈ Ο‰ ↦ βˆ…) ∈ β„•βˆž
65fconst6 5415 . . . . . . . . . . . . 13 (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}):π‘§βŸΆβ„•βˆž
76a1i 9 . . . . . . . . . . . 12 (𝑧 βŠ† {βˆ…} β†’ (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}):π‘§βŸΆβ„•βˆž)
8 ssel 3149 . . . . . . . . . . . . . . . . . 18 (𝑧 βŠ† {βˆ…} β†’ (𝑒 ∈ 𝑧 β†’ 𝑒 ∈ {βˆ…}))
9 elsni 3610 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ {βˆ…} β†’ 𝑒 = βˆ…)
108, 9syl6 33 . . . . . . . . . . . . . . . . 17 (𝑧 βŠ† {βˆ…} β†’ (𝑒 ∈ 𝑧 β†’ 𝑒 = βˆ…))
11 ssel 3149 . . . . . . . . . . . . . . . . . 18 (𝑧 βŠ† {βˆ…} β†’ (𝑣 ∈ 𝑧 β†’ 𝑣 ∈ {βˆ…}))
12 elsni 3610 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {βˆ…} β†’ 𝑣 = βˆ…)
1311, 12syl6 33 . . . . . . . . . . . . . . . . 17 (𝑧 βŠ† {βˆ…} β†’ (𝑣 ∈ 𝑧 β†’ 𝑣 = βˆ…))
1410, 13anim12d 335 . . . . . . . . . . . . . . . 16 (𝑧 βŠ† {βˆ…} β†’ ((𝑒 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) β†’ (𝑒 = βˆ… ∧ 𝑣 = βˆ…)))
15 eqtr3 2197 . . . . . . . . . . . . . . . 16 ((𝑒 = βˆ… ∧ 𝑣 = βˆ…) β†’ 𝑒 = 𝑣)
1614, 15syl6 33 . . . . . . . . . . . . . . 15 (𝑧 βŠ† {βˆ…} β†’ ((𝑒 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) β†’ 𝑒 = 𝑣))
1716imp 124 . . . . . . . . . . . . . 14 ((𝑧 βŠ† {βˆ…} ∧ (𝑒 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) β†’ 𝑒 = 𝑣)
1817a1d 22 . . . . . . . . . . . . 13 ((𝑧 βŠ† {βˆ…} ∧ (𝑒 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) β†’ (((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘’) = ((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘£) β†’ 𝑒 = 𝑣))
1918ralrimivva 2559 . . . . . . . . . . . 12 (𝑧 βŠ† {βˆ…} β†’ βˆ€π‘’ ∈ 𝑧 βˆ€π‘£ ∈ 𝑧 (((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘’) = ((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘£) β†’ 𝑒 = 𝑣))
20 dff13 5768 . . . . . . . . . . . 12 ((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}):𝑧–1-1β†’β„•βˆž ↔ ((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}):π‘§βŸΆβ„•βˆž ∧ βˆ€π‘’ ∈ 𝑧 βˆ€π‘£ ∈ 𝑧 (((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘’) = ((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)})β€˜π‘£) β†’ 𝑒 = 𝑣)))
217, 19, 20sylanbrc 417 . . . . . . . . . . 11 (𝑧 βŠ† {βˆ…} β†’ (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}):𝑧–1-1β†’β„•βˆž)
22 exmidsbthrlem.s . . . . . . . . . . . . 13 𝑆 = (𝑝 ∈ β„•βˆž ↦ (𝑖 ∈ Ο‰ ↦ if(𝑖 = βˆ…, 1o, (π‘β€˜βˆͺ 𝑖))))
2322peano4nninf 14725 . . . . . . . . . . . 12 𝑆:β„•βˆžβ€“1-1β†’β„•βˆž
2423a1i 9 . . . . . . . . . . 11 (𝑧 βŠ† {βˆ…} β†’ 𝑆:β„•βˆžβ€“1-1β†’β„•βˆž)
25 disj 3471 . . . . . . . . . . . . 13 ((ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) ∩ ran 𝑆) = βˆ… ↔ βˆ€π‘Ž ∈ ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) Β¬ π‘Ž ∈ ran 𝑆)
2622peano3nninf 14726 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ β„•βˆž β†’ (π‘†β€˜π‘) β‰  (π‘˜ ∈ Ο‰ ↦ βˆ…))
27 eqidd 2178 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 𝑖 β†’ βˆ… = βˆ…)
2827cbvmptv 4099 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ Ο‰ ↦ βˆ…) = (𝑖 ∈ Ο‰ ↦ βˆ…)
2928neeq2i 2363 . . . . . . . . . . . . . . . . . . 19 ((π‘†β€˜π‘) β‰  (π‘˜ ∈ Ο‰ ↦ βˆ…) ↔ (π‘†β€˜π‘) β‰  (𝑖 ∈ Ο‰ ↦ βˆ…))
3026, 29sylib 122 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ β„•βˆž β†’ (π‘†β€˜π‘) β‰  (𝑖 ∈ Ο‰ ↦ βˆ…))
3130neneqd 2368 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ β„•βˆž β†’ Β¬ (π‘†β€˜π‘) = (𝑖 ∈ Ο‰ ↦ βˆ…))
3231nrex 2569 . . . . . . . . . . . . . . . 16 Β¬ βˆƒπ‘ ∈ β„•βˆž (π‘†β€˜π‘) = (𝑖 ∈ Ο‰ ↦ βˆ…)
33 f1dm 5426 . . . . . . . . . . . . . . . . . 18 (𝑆:β„•βˆžβ€“1-1β†’β„•βˆž β†’ dom 𝑆 = β„•βˆž)
3423, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 dom 𝑆 = β„•βˆž
35 eqcom 2179 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ Ο‰ ↦ βˆ…) = (π‘†β€˜π‘) ↔ (π‘†β€˜π‘) = (𝑖 ∈ Ο‰ ↦ βˆ…))
3634, 35rexeqbii 2490 . . . . . . . . . . . . . . . 16 (βˆƒπ‘ ∈ dom 𝑆(𝑖 ∈ Ο‰ ↦ βˆ…) = (π‘†β€˜π‘) ↔ βˆƒπ‘ ∈ β„•βˆž (π‘†β€˜π‘) = (𝑖 ∈ Ο‰ ↦ βˆ…))
3732, 36mtbir 671 . . . . . . . . . . . . . . 15 Β¬ βˆƒπ‘ ∈ dom 𝑆(𝑖 ∈ Ο‰ ↦ βˆ…) = (π‘†β€˜π‘)
3822funmpt2 5255 . . . . . . . . . . . . . . . 16 Fun 𝑆
39 elrnrexdm 5655 . . . . . . . . . . . . . . . 16 (Fun 𝑆 β†’ ((𝑖 ∈ Ο‰ ↦ βˆ…) ∈ ran 𝑆 β†’ βˆƒπ‘ ∈ dom 𝑆(𝑖 ∈ Ο‰ ↦ βˆ…) = (π‘†β€˜π‘)))
4038, 39ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑖 ∈ Ο‰ ↦ βˆ…) ∈ ran 𝑆 β†’ βˆƒπ‘ ∈ dom 𝑆(𝑖 ∈ Ο‰ ↦ βˆ…) = (π‘†β€˜π‘))
4137, 40mto 662 . . . . . . . . . . . . . 14 Β¬ (𝑖 ∈ Ο‰ ↦ βˆ…) ∈ ran 𝑆
42 rnxpss 5060 . . . . . . . . . . . . . . . . 17 ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) βŠ† {(𝑖 ∈ Ο‰ ↦ βˆ…)}
4342sseli 3151 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) β†’ π‘Ž ∈ {(𝑖 ∈ Ο‰ ↦ βˆ…)})
44 elsni 3610 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ {(𝑖 ∈ Ο‰ ↦ βˆ…)} β†’ π‘Ž = (𝑖 ∈ Ο‰ ↦ βˆ…))
4543, 44syl 14 . . . . . . . . . . . . . . 15 (π‘Ž ∈ ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) β†’ π‘Ž = (𝑖 ∈ Ο‰ ↦ βˆ…))
4645eleq1d 2246 . . . . . . . . . . . . . 14 (π‘Ž ∈ ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) β†’ (π‘Ž ∈ ran 𝑆 ↔ (𝑖 ∈ Ο‰ ↦ βˆ…) ∈ ran 𝑆))
4741, 46mtbiri 675 . . . . . . . . . . . . 13 (π‘Ž ∈ ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) β†’ Β¬ π‘Ž ∈ ran 𝑆)
4825, 47mprgbir 2535 . . . . . . . . . . . 12 (ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) ∩ ran 𝑆) = βˆ…
4948a1i 9 . . . . . . . . . . 11 (𝑧 βŠ† {βˆ…} β†’ (ran (𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}) ∩ ran 𝑆) = βˆ…)
5021, 24, 49casef1 7088 . . . . . . . . . 10 (𝑧 βŠ† {βˆ…} β†’ case((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}), 𝑆):(𝑧 βŠ” β„•βˆž)–1-1β†’β„•βˆž)
51 f1domg 6757 . . . . . . . . . 10 (β„•βˆž ∈ V β†’ (case((𝑧 Γ— {(𝑖 ∈ Ο‰ ↦ βˆ…)}), 𝑆):(𝑧 βŠ” β„•βˆž)–1-1β†’β„•βˆž β†’ (𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž))
522, 50, 51mpsyl 65 . . . . . . . . 9 (𝑧 βŠ† {βˆ…} β†’ (𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž)
5352adantl 277 . . . . . . . 8 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ (𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž)
54 inrresf1 7060 . . . . . . . . 9 (inr β†Ύ β„•βˆž):β„•βˆžβ€“1-1β†’(𝑧 βŠ” β„•βˆž)
55 vex 2740 . . . . . . . . . . 11 𝑧 ∈ V
56 djuex 7041 . . . . . . . . . . 11 ((𝑧 ∈ V ∧ β„•βˆž ∈ V) β†’ (𝑧 βŠ” β„•βˆž) ∈ V)
5755, 2, 56mp2an 426 . . . . . . . . . 10 (𝑧 βŠ” β„•βˆž) ∈ V
5857f1dom 6759 . . . . . . . . 9 ((inr β†Ύ β„•βˆž):β„•βˆžβ€“1-1β†’(𝑧 βŠ” β„•βˆž) β†’ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž))
5954, 58ax-mp 5 . . . . . . . 8 β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)
6053, 59jctir 313 . . . . . . 7 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ ((𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž ∧ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)))
61 breq12 4008 . . . . . . . . . . 11 ((π‘₯ = (𝑧 βŠ” β„•βˆž) ∧ 𝑦 = β„•βˆž) β†’ (π‘₯ β‰Ό 𝑦 ↔ (𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž))
62 breq12 4008 . . . . . . . . . . . 12 ((𝑦 = β„•βˆž ∧ π‘₯ = (𝑧 βŠ” β„•βˆž)) β†’ (𝑦 β‰Ό π‘₯ ↔ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)))
6362ancoms 268 . . . . . . . . . . 11 ((π‘₯ = (𝑧 βŠ” β„•βˆž) ∧ 𝑦 = β„•βˆž) β†’ (𝑦 β‰Ό π‘₯ ↔ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)))
6461, 63anbi12d 473 . . . . . . . . . 10 ((π‘₯ = (𝑧 βŠ” β„•βˆž) ∧ 𝑦 = β„•βˆž) β†’ ((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) ↔ ((𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž ∧ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž))))
65 breq12 4008 . . . . . . . . . 10 ((π‘₯ = (𝑧 βŠ” β„•βˆž) ∧ 𝑦 = β„•βˆž) β†’ (π‘₯ β‰ˆ 𝑦 ↔ (𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž))
6664, 65imbi12d 234 . . . . . . . . 9 ((π‘₯ = (𝑧 βŠ” β„•βˆž) ∧ 𝑦 = β„•βˆž) β†’ (((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ↔ (((𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž ∧ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)) β†’ (𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž)))
6766spc2gv 2828 . . . . . . . 8 (((𝑧 βŠ” β„•βˆž) ∈ V ∧ β„•βˆž ∈ V) β†’ (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ (((𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž ∧ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)) β†’ (𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž)))
6857, 2, 67mp2an 426 . . . . . . 7 (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ (((𝑧 βŠ” β„•βˆž) β‰Ό β„•βˆž ∧ β„•βˆž β‰Ό (𝑧 βŠ” β„•βˆž)) β†’ (𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž))
691, 60, 68sylc 62 . . . . . 6 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ (𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž)
70 bren 6746 . . . . . 6 ((𝑧 βŠ” β„•βˆž) β‰ˆ β„•βˆž ↔ βˆƒπ‘“ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž)
7169, 70sylib 122 . . . . 5 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ βˆƒπ‘“ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž)
72 nninfomni 14738 . . . . . . . . 9 β„•βˆž ∈ Omni
7372a1i 9 . . . . . . . 8 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ β„•βˆž ∈ Omni)
74 f1ocnv 5474 . . . . . . . . . 10 (𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž β†’ ◑𝑓:β„•βˆžβ€“1-1-ontoβ†’(𝑧 βŠ” β„•βˆž))
75 f1ofo 5468 . . . . . . . . . 10 (◑𝑓:β„•βˆžβ€“1-1-ontoβ†’(𝑧 βŠ” β„•βˆž) β†’ ◑𝑓:β„•βˆžβ€“ontoβ†’(𝑧 βŠ” β„•βˆž))
7674, 75syl 14 . . . . . . . . 9 (𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž β†’ ◑𝑓:β„•βˆžβ€“ontoβ†’(𝑧 βŠ” β„•βˆž))
7776adantl 277 . . . . . . . 8 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ ◑𝑓:β„•βˆžβ€“ontoβ†’(𝑧 βŠ” β„•βˆž))
7873, 77fodjuomni 7146 . . . . . . 7 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ (βˆƒπ‘€ 𝑀 ∈ 𝑧 ∨ 𝑧 = βˆ…))
79 sssnm 3754 . . . . . . . . . 10 (βˆƒπ‘€ 𝑀 ∈ 𝑧 β†’ (𝑧 βŠ† {βˆ…} ↔ 𝑧 = {βˆ…}))
8079biimpcd 159 . . . . . . . . 9 (𝑧 βŠ† {βˆ…} β†’ (βˆƒπ‘€ 𝑀 ∈ 𝑧 β†’ 𝑧 = {βˆ…}))
8180ad2antlr 489 . . . . . . . 8 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ (βˆƒπ‘€ 𝑀 ∈ 𝑧 β†’ 𝑧 = {βˆ…}))
8281orim1d 787 . . . . . . 7 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ ((βˆƒπ‘€ 𝑀 ∈ 𝑧 ∨ 𝑧 = βˆ…) β†’ (𝑧 = {βˆ…} ∨ 𝑧 = βˆ…)))
8378, 82mpd 13 . . . . . 6 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ (𝑧 = {βˆ…} ∨ 𝑧 = βˆ…))
8483orcomd 729 . . . . 5 (((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) ∧ 𝑓:(𝑧 βŠ” β„•βˆž)–1-1-ontoβ†’β„•βˆž) β†’ (𝑧 = βˆ… ∨ 𝑧 = {βˆ…}))
8571, 84exlimddv 1898 . . . 4 ((βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) ∧ 𝑧 βŠ† {βˆ…}) β†’ (𝑧 = βˆ… ∨ 𝑧 = {βˆ…}))
8685ex 115 . . 3 (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ (𝑧 βŠ† {βˆ…} β†’ (𝑧 = βˆ… ∨ 𝑧 = {βˆ…})))
8786alrimiv 1874 . 2 (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ βˆ€π‘§(𝑧 βŠ† {βˆ…} β†’ (𝑧 = βˆ… ∨ 𝑧 = {βˆ…})))
88 exmid01 4198 . 2 (EXMID ↔ βˆ€π‘§(𝑧 βŠ† {βˆ…} β†’ (𝑧 = βˆ… ∨ 𝑧 = {βˆ…})))
8987, 88sylibr 134 1 (βˆ€π‘₯βˆ€π‘¦((π‘₯ β‰Ό 𝑦 ∧ 𝑦 β‰Ό π‘₯) β†’ π‘₯ β‰ˆ 𝑦) β†’ EXMID)
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  βˆ€wal 1351   = wceq 1353  βˆƒwex 1492   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2737   ∩ cin 3128   βŠ† wss 3129  βˆ…c0 3422  ifcif 3534  {csn 3592  βˆͺ cuni 3809   class class class wbr 4003   ↦ cmpt 4064  EXMIDwem 4194  Ο‰com 4589   Γ— cxp 4624  β—‘ccnv 4625  dom cdm 4626  ran crn 4627   β†Ύ cres 4628  Fun wfun 5210  βŸΆwf 5212  β€“1-1β†’wf1 5213  β€“ontoβ†’wfo 5214  β€“1-1-ontoβ†’wf1o 5215  β€˜cfv 5216  1oc1o 6409   β‰ˆ cen 6737   β‰Ό cdom 6738   βŠ” cdju 7035  inrcinr 7044  casecdjucase 7081  β„•βˆžxnninf 7117  Omnicomni 7131
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 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
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 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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-exmid 4195  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-1o 6416  df-2o 6417  df-map 6649  df-en 6740  df-dom 6741  df-dju 7036  df-inl 7045  df-inr 7046  df-case 7082  df-nninf 7118  df-omni 7132
This theorem is referenced by:  exmidsbthr  14741
  Copyright terms: Public domain W3C validator