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

Theorem acexmidlemcase 5534
Description: Lemma for acexmid 5538. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at 𝐴 equals {∅}, (2) the choice function evaluated at 𝐵 equals , and (3) the choice function evaluated at 𝐴 equals and the choice function evaluated at 𝐵 equals {∅}.

Because of the way we represent the choice function 𝑦, the choice function evaluated at 𝐴 is (𝑣𝐴𝑢𝑦(𝐴𝑢𝑣𝑢)) and the choice function evaluated at 𝐵 is (𝑣𝐵𝑢𝑦(𝐵𝑢𝑣𝑢)). Other than the difference in notation these work just as (𝑦𝐴) and (𝑦𝐵) would if 𝑦 were a function as defined by df-fun 4931.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at 𝐴 equals {∅}, then {∅} ∈ 𝐴 and likewise for 𝐵.

(Contributed by Jim Kingdon, 7-Aug-2019.)

Hypotheses
Ref Expression
acexmidlem.a 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}
acexmidlem.b 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}
acexmidlem.c 𝐶 = {𝐴, 𝐵}
Assertion
Ref Expression
acexmidlemcase (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝑢,𝐴   𝑥,𝐵,𝑦,𝑧,𝑣,𝑢   𝑥,𝐶,𝑦,𝑧,𝑣,𝑢   𝜑,𝑥,𝑦,𝑧,𝑣,𝑢

Proof of Theorem acexmidlemcase
StepHypRef Expression
1 acexmidlem.a . . . . . . . . . . . . . 14 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}
2 onsucelsucexmidlem 4281 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} ∈ On
31, 2eqeltri 2126 . . . . . . . . . . . . 13 𝐴 ∈ On
4 prid1g 3501 . . . . . . . . . . . . 13 (𝐴 ∈ On → 𝐴 ∈ {𝐴, 𝐵})
53, 4ax-mp 7 . . . . . . . . . . . 12 𝐴 ∈ {𝐴, 𝐵}
6 acexmidlem.c . . . . . . . . . . . 12 𝐶 = {𝐴, 𝐵}
75, 6eleqtrri 2129 . . . . . . . . . . 11 𝐴𝐶
8 eleq1 2116 . . . . . . . . . . . . . . 15 (𝑧 = 𝐴 → (𝑧𝑢𝐴𝑢))
98anbi1d 446 . . . . . . . . . . . . . 14 (𝑧 = 𝐴 → ((𝑧𝑢𝑣𝑢) ↔ (𝐴𝑢𝑣𝑢)))
109rexbidv 2344 . . . . . . . . . . . . 13 (𝑧 = 𝐴 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1110reueqd 2532 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1211rspcv 2669 . . . . . . . . . . 11 (𝐴𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
137, 12ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢))
14 riotacl 5509 . . . . . . . . . 10 (∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
1513, 14syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
16 elrabi 2717 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
1716, 1eleq2s 2148 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
18 elpri 3425 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
1915, 17, 183syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
20 eleq1 2116 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 ↔ {∅} ∈ 𝐴))
2115, 20syl5ibcom 148 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → {∅} ∈ 𝐴))
2221orim2d 712 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴)))
2319, 22mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴))
24 acexmidlem.b . . . . . . . . . . . . . 14 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}
25 pp0ex 3967 . . . . . . . . . . . . . . 15 {∅, {∅}} ∈ V
2625rabex 3928 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} ∈ V
2724, 26eqeltri 2126 . . . . . . . . . . . . 13 𝐵 ∈ V
2827prid2 3504 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
2928, 6eleqtrri 2129 . . . . . . . . . . 11 𝐵𝐶
30 eleq1 2116 . . . . . . . . . . . . . . 15 (𝑧 = 𝐵 → (𝑧𝑢𝐵𝑢))
3130anbi1d 446 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → ((𝑧𝑢𝑣𝑢) ↔ (𝐵𝑢𝑣𝑢)))
3231rexbidv 2344 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3332reueqd 2532 . . . . . . . . . . . 12 (𝑧 = 𝐵 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3433rspcv 2669 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3529, 34ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢))
36 riotacl 5509 . . . . . . . . . 10 (∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
3735, 36syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
38 elrabi 2717 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
3938, 24eleq2s 2148 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
40 elpri 3425 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4137, 39, 403syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
42 eleq1 2116 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 ↔ ∅ ∈ 𝐵))
4337, 42syl5ibcom 148 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ∅ ∈ 𝐵))
4443orim1d 711 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
4541, 44mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4623, 45jca 294 . . . . . 6 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
47 anddi 745 . . . . . 6 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
4846, 47sylib 131 . . . . 5 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
49 simpl 106 . . . . . . 7 (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) → {∅} ∈ 𝐴)
50 simpl 106 . . . . . . 7 (({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → {∅} ∈ 𝐴)
5149, 50jaoi 646 . . . . . 6 ((({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → {∅} ∈ 𝐴)
5251orim2i 688 . . . . 5 (((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5348, 52syl 14 . . . 4 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5453orcomd 658 . . 3 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
55 simpr 107 . . . . 5 (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) → ∅ ∈ 𝐵)
5655orim1i 687 . . . 4 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
5756orim2i 688 . . 3 (({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
5854, 57syl 14 . 2 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
59 3orass 899 . 2 (({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
6058, 59sylibr 141 1 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wo 639  w3o 895   = wceq 1259  wcel 1409  wral 2323  wrex 2324  ∃!wreu 2325  {crab 2327  Vcvv 2574  c0 3251  {csn 3402  {cpr 3403  Oncon0 4127  crio 5494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-nul 3910  ax-pow 3954
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-uni 3608  df-tr 3882  df-iord 4130  df-on 4132  df-suc 4135  df-iota 4894  df-riota 5495
This theorem is referenced by:  acexmidlem1  5535
  Copyright terms: Public domain W3C validator