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

Theorem acexmidlemcase 5559
Description: Lemma for acexmid 5563. 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 4954.

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 4300 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} ∈ On
31, 2eqeltri 2155 . . . . . . . . . . . . 13 𝐴 ∈ On
4 prid1g 3514 . . . . . . . . . . . . 13 (𝐴 ∈ On → 𝐴 ∈ {𝐴, 𝐵})
53, 4ax-mp 7 . . . . . . . . . . . 12 𝐴 ∈ {𝐴, 𝐵}
6 acexmidlem.c . . . . . . . . . . . 12 𝐶 = {𝐴, 𝐵}
75, 6eleqtrri 2158 . . . . . . . . . . 11 𝐴𝐶
8 eleq1 2145 . . . . . . . . . . . . . . 15 (𝑧 = 𝐴 → (𝑧𝑢𝐴𝑢))
98anbi1d 453 . . . . . . . . . . . . . 14 (𝑧 = 𝐴 → ((𝑧𝑢𝑣𝑢) ↔ (𝐴𝑢𝑣𝑢)))
109rexbidv 2374 . . . . . . . . . . . . 13 (𝑧 = 𝐴 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1110reueqd 2564 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1211rspcv 2706 . . . . . . . . . . 11 (𝐴𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
137, 12ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢))
14 riotacl 5534 . . . . . . . . . 10 (∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
1513, 14syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
16 elrabi 2754 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
1716, 1eleq2s 2177 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
18 elpri 3439 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
1915, 17, 183syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
20 eleq1 2145 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 ↔ {∅} ∈ 𝐴))
2115, 20syl5ibcom 153 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → {∅} ∈ 𝐴))
2221orim2d 735 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴)))
2319, 22mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴))
24 acexmidlem.b . . . . . . . . . . . . . 14 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}
25 pp0ex 3980 . . . . . . . . . . . . . . 15 {∅, {∅}} ∈ V
2625rabex 3942 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} ∈ V
2724, 26eqeltri 2155 . . . . . . . . . . . . 13 𝐵 ∈ V
2827prid2 3517 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
2928, 6eleqtrri 2158 . . . . . . . . . . 11 𝐵𝐶
30 eleq1 2145 . . . . . . . . . . . . . . 15 (𝑧 = 𝐵 → (𝑧𝑢𝐵𝑢))
3130anbi1d 453 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → ((𝑧𝑢𝑣𝑢) ↔ (𝐵𝑢𝑣𝑢)))
3231rexbidv 2374 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3332reueqd 2564 . . . . . . . . . . . 12 (𝑧 = 𝐵 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3433rspcv 2706 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3529, 34ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢))
36 riotacl 5534 . . . . . . . . . 10 (∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
3735, 36syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
38 elrabi 2754 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
3938, 24eleq2s 2177 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
40 elpri 3439 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4137, 39, 403syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
42 eleq1 2145 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 ↔ ∅ ∈ 𝐵))
4337, 42syl5ibcom 153 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ∅ ∈ 𝐵))
4443orim1d 734 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
4541, 44mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4623, 45jca 300 . . . . . 6 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
47 anddi 768 . . . . . 6 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
4846, 47sylib 120 . . . . 5 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
49 simpl 107 . . . . . . 7 (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) → {∅} ∈ 𝐴)
50 simpl 107 . . . . . . 7 (({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → {∅} ∈ 𝐴)
5149, 50jaoi 669 . . . . . 6 ((({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → {∅} ∈ 𝐴)
5251orim2i 711 . . . . 5 (((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5348, 52syl 14 . . . 4 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5453orcomd 681 . . 3 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
55 simpr 108 . . . . 5 (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) → ∅ ∈ 𝐵)
5655orim1i 710 . . . 4 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
5756orim2i 711 . . 3 (({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
5854, 57syl 14 . 2 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
59 3orass 923 . 2 (({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
6058, 59sylibr 132 1 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662  w3o 919   = wceq 1285  wcel 1434  wral 2353  wrex 2354  ∃!wreu 2355  {crab 2357  Vcvv 2610  c0 3267  {csn 3416  {cpr 3417  Oncon0 4146  crio 5519
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-nul 3924  ax-pow 3968
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2825  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-uni 3622  df-tr 3896  df-iord 4149  df-on 4151  df-suc 4154  df-iota 4917  df-riota 5520
This theorem is referenced by:  acexmidlem1  5560
  Copyright terms: Public domain W3C validator