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

Theorem acexmidlemcase 5507
Description: Lemma for acexmid 5511. 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 4904.

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 4254 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} ∈ On
31, 2eqeltri 2110 . . . . . . . . . . . . 13 𝐴 ∈ On
4 prid1g 3474 . . . . . . . . . . . . 13 (𝐴 ∈ On → 𝐴 ∈ {𝐴, 𝐵})
53, 4ax-mp 7 . . . . . . . . . . . 12 𝐴 ∈ {𝐴, 𝐵}
6 acexmidlem.c . . . . . . . . . . . 12 𝐶 = {𝐴, 𝐵}
75, 6eleqtrri 2113 . . . . . . . . . . 11 𝐴𝐶
8 eleq1 2100 . . . . . . . . . . . . . . 15 (𝑧 = 𝐴 → (𝑧𝑢𝐴𝑢))
98anbi1d 438 . . . . . . . . . . . . . 14 (𝑧 = 𝐴 → ((𝑧𝑢𝑣𝑢) ↔ (𝐴𝑢𝑣𝑢)))
109rexbidv 2327 . . . . . . . . . . . . 13 (𝑧 = 𝐴 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1110reueqd 2515 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
1211rspcv 2652 . . . . . . . . . . 11 (𝐴𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)))
137, 12ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢))
14 riotacl 5482 . . . . . . . . . 10 (∃!𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
1513, 14syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴)
16 elrabi 2695 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
1716, 1eleq2s 2132 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 → (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}})
18 elpri 3398 . . . . . . . . 9 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
1915, 17, 183syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}))
20 eleq1 2100 . . . . . . . . . 10 ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) ∈ 𝐴 ↔ {∅} ∈ 𝐴))
2115, 20syl5ibcom 144 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅} → {∅} ∈ 𝐴))
2221orim2d 702 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = {∅}) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴)))
2319, 22mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴))
24 acexmidlem.b . . . . . . . . . . . . . 14 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}
25 pp0ex 3940 . . . . . . . . . . . . . . 15 {∅, {∅}} ∈ V
2625rabex 3901 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} ∈ V
2724, 26eqeltri 2110 . . . . . . . . . . . . 13 𝐵 ∈ V
2827prid2 3477 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
2928, 6eleqtrri 2113 . . . . . . . . . . 11 𝐵𝐶
30 eleq1 2100 . . . . . . . . . . . . . . 15 (𝑧 = 𝐵 → (𝑧𝑢𝐵𝑢))
3130anbi1d 438 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → ((𝑧𝑢𝑣𝑢) ↔ (𝐵𝑢𝑣𝑢)))
3231rexbidv 2327 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3332reueqd 2515 . . . . . . . . . . . 12 (𝑧 = 𝐵 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3433rspcv 2652 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)))
3529, 34ax-mp 7 . . . . . . . . . 10 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢))
36 riotacl 5482 . . . . . . . . . 10 (∃!𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
3735, 36syl 14 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵)
38 elrabi 2695 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
3938, 24eleq2s 2132 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 → (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}})
40 elpri 3398 . . . . . . . . 9 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ {∅, {∅}} → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4137, 39, 403syl 17 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
42 eleq1 2100 . . . . . . . . . 10 ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) ∈ 𝐵 ↔ ∅ ∈ 𝐵))
4337, 42syl5ibcom 144 . . . . . . . . 9 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ → ∅ ∈ 𝐵))
4443orim1d 701 . . . . . . . 8 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = ∅ ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
4541, 44mpd 13 . . . . . . 7 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))
4623, 45jca 290 . . . . . 6 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
47 anddi 734 . . . . . 6 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∨ {∅} ∈ 𝐴) ∧ (∅ ∈ 𝐵 ∨ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
4846, 47sylib 127 . . . . 5 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
49 simpl 102 . . . . . . 7 (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) → {∅} ∈ 𝐴)
50 simpl 102 . . . . . . 7 (({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}) → {∅} ∈ 𝐴)
5149, 50jaoi 636 . . . . . 6 ((({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → {∅} ∈ 𝐴)
5251orim2i 678 . . . . 5 (((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ (({∅} ∈ 𝐴 ∧ ∅ ∈ 𝐵) ∨ ({∅} ∈ 𝐴 ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5348, 52syl 14 . . . 4 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ∨ {∅} ∈ 𝐴))
5453orcomd 648 . . 3 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
55 simpr 103 . . . . 5 (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) → ∅ ∈ 𝐵)
5655orim1i 677 . . . 4 ((((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) → (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
5756orim2i 678 . . 3 (({∅} ∈ 𝐴 ∨ (((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ ∅ ∈ 𝐵) ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
5854, 57syl 14 . 2 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
59 3orass 888 . 2 (({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})) ↔ ({∅} ∈ 𝐴 ∨ (∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅}))))
6058, 59sylibr 137 1 (∀𝑧𝐶 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((𝑣𝐴𝑢𝑦 (𝐴𝑢𝑣𝑢)) = ∅ ∧ (𝑣𝐵𝑢𝑦 (𝐵𝑢𝑣𝑢)) = {∅})))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wo 629  w3o 884   = wceq 1243  wcel 1393  wral 2306  wrex 2307  ∃!wreu 2308  {crab 2310  Vcvv 2557  c0 3224  {csn 3375  {cpr 3376  Oncon0 4100  crio 5467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-nul 3883  ax-pow 3927
This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-uni 3581  df-tr 3855  df-iord 4103  df-on 4105  df-suc 4108  df-iota 4867  df-riota 5468
This theorem is referenced by:  acexmidlem1  5508
  Copyright terms: Public domain W3C validator