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

Theorem exmidaclem 7057
Description: Lemma for exmidac 7058. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
Hypotheses
Ref Expression
exmidaclem.a 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}
exmidaclem.b 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}
exmidaclem.c 𝐶 = {𝐴, 𝐵}
Assertion
Ref Expression
exmidaclem (CHOICEEXMID)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem exmidaclem
Dummy variables 𝑧 𝑓 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 108 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → CHOICE)
2 exmidaclem.c . . . . . 6 𝐶 = {𝐴, 𝐵}
3 exmidaclem.a . . . . . . . 8 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}
4 pp0ex 4108 . . . . . . . . 9 {∅, {∅}} ∈ V
54rabex 4067 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ∈ V
63, 5eqeltri 2210 . . . . . . 7 𝐴 ∈ V
7 exmidaclem.b . . . . . . . 8 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}
84rabex 4067 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ∈ V
97, 8eqeltri 2210 . . . . . . 7 𝐵 ∈ V
10 prexg 4128 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
116, 9, 10mp2an 422 . . . . . 6 {𝐴, 𝐵} ∈ V
122, 11eqeltri 2210 . . . . 5 𝐶 ∈ V
1312a1i 9 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → 𝐶 ∈ V)
14 simpr 109 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧𝐶)
1514, 2eleqtrdi 2230 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧 ∈ {𝐴, 𝐵})
16 elpri 3545 . . . . . 6 (𝑧 ∈ {𝐴, 𝐵} → (𝑧 = 𝐴𝑧 = 𝐵))
17 0ex 4050 . . . . . . . . . . 11 ∅ ∈ V
1817prid1 3624 . . . . . . . . . 10 ∅ ∈ {∅, {∅}}
19 eqid 2137 . . . . . . . . . . 11 ∅ = ∅
2019orci 720 . . . . . . . . . 10 (∅ = ∅ ∨ 𝑦 = {∅})
21 eqeq1 2144 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ = ∅))
2221orbi1d 780 . . . . . . . . . . 11 (𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ (∅ = ∅ ∨ 𝑦 = {∅})))
2322, 3elrab2 2838 . . . . . . . . . 10 (∅ ∈ 𝐴 ↔ (∅ ∈ {∅, {∅}} ∧ (∅ = ∅ ∨ 𝑦 = {∅})))
2418, 20, 23mpbir2an 926 . . . . . . . . 9 ∅ ∈ 𝐴
25 eleq2 2201 . . . . . . . . 9 (𝑧 = 𝐴 → (∅ ∈ 𝑧 ↔ ∅ ∈ 𝐴))
2624, 25mpbiri 167 . . . . . . . 8 (𝑧 = 𝐴 → ∅ ∈ 𝑧)
27 elex2 2697 . . . . . . . 8 (∅ ∈ 𝑧 → ∃𝑤 𝑤𝑧)
2826, 27syl 14 . . . . . . 7 (𝑧 = 𝐴 → ∃𝑤 𝑤𝑧)
29 p0ex 4107 . . . . . . . . . . 11 {∅} ∈ V
3029prid2 3625 . . . . . . . . . 10 {∅} ∈ {∅, {∅}}
31 eqid 2137 . . . . . . . . . . 11 {∅} = {∅}
3231orci 720 . . . . . . . . . 10 ({∅} = {∅} ∨ 𝑦 = {∅})
33 eqeq1 2144 . . . . . . . . . . . 12 (𝑥 = {∅} → (𝑥 = {∅} ↔ {∅} = {∅}))
3433orbi1d 780 . . . . . . . . . . 11 (𝑥 = {∅} → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ({∅} = {∅} ∨ 𝑦 = {∅})))
3534, 7elrab2 2838 . . . . . . . . . 10 ({∅} ∈ 𝐵 ↔ ({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅} ∨ 𝑦 = {∅})))
3630, 32, 35mpbir2an 926 . . . . . . . . 9 {∅} ∈ 𝐵
37 eleq2 2201 . . . . . . . . 9 (𝑧 = 𝐵 → ({∅} ∈ 𝑧 ↔ {∅} ∈ 𝐵))
3836, 37mpbiri 167 . . . . . . . 8 (𝑧 = 𝐵 → {∅} ∈ 𝑧)
39 elex2 2697 . . . . . . . 8 ({∅} ∈ 𝑧 → ∃𝑤 𝑤𝑧)
4038, 39syl 14 . . . . . . 7 (𝑧 = 𝐵 → ∃𝑤 𝑤𝑧)
4128, 40jaoi 705 . . . . . 6 ((𝑧 = 𝐴𝑧 = 𝐵) → ∃𝑤 𝑤𝑧)
4215, 16, 413syl 17 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → ∃𝑤 𝑤𝑧)
4342ralrimiva 2503 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → ∀𝑧𝐶𝑤 𝑤𝑧)
441, 13, 43acfun 7056 . . 3 ((CHOICE𝑦 ⊆ {∅}) → ∃𝑓(𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧))
45 0nep0 4084 . . . . . . . . . 10 ∅ ≠ {∅}
4645neii 2308 . . . . . . . . 9 ¬ ∅ = {∅}
47 simplr 519 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐴) = ∅)
48 simpr 109 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐵) = {∅})
4947, 48eqeq12d 2152 . . . . . . . . 9 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ((𝑓𝐴) = (𝑓𝐵) ↔ ∅ = {∅}))
5046, 49mtbiri 664 . . . . . . . 8 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ¬ (𝑓𝐴) = (𝑓𝐵))
51 olc 700 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = ∅ ∨ 𝑦 = {∅}))
5251ralrimivw 2504 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
53 rabid2 2605 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
5452, 53sylibr 133 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})})
5554, 3syl6eqr 2188 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐴)
56 olc 700 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = {∅} ∨ 𝑦 = {∅}))
5756ralrimivw 2504 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
58 rabid2 2605 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
5957, 58sylibr 133 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})})
6059, 7syl6eqr 2188 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐵)
6155, 60eqtr3d 2172 . . . . . . . . 9 (𝑦 = {∅} → 𝐴 = 𝐵)
6261fveq2d 5418 . . . . . . . 8 (𝑦 = {∅} → (𝑓𝐴) = (𝑓𝐵))
6350, 62nsyl 617 . . . . . . 7 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ¬ 𝑦 = {∅})
6463olcd 723 . . . . . 6 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
65 simpr 109 . . . . . . 7 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
6665orcd 722 . . . . . 6 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ 𝑦 = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
67 fveq2 5414 . . . . . . . . . . 11 (𝑧 = 𝐵 → (𝑓𝑧) = (𝑓𝐵))
68 id 19 . . . . . . . . . . 11 (𝑧 = 𝐵𝑧 = 𝐵)
6967, 68eleq12d 2208 . . . . . . . . . 10 (𝑧 = 𝐵 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐵) ∈ 𝐵))
70 simprr 521 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)
719prid2 3625 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
7271, 2eleqtrri 2213 . . . . . . . . . . 11 𝐵𝐶
7372a1i 9 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐵𝐶)
7469, 70, 73rspcdva 2789 . . . . . . . . 9 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐵) ∈ 𝐵)
75 eqeq1 2144 . . . . . . . . . . 11 (𝑥 = (𝑓𝐵) → (𝑥 = {∅} ↔ (𝑓𝐵) = {∅}))
7675orbi1d 780 . . . . . . . . . 10 (𝑥 = (𝑓𝐵) → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7776, 7elrab2 2838 . . . . . . . . 9 ((𝑓𝐵) ∈ 𝐵 ↔ ((𝑓𝐵) ∈ {∅, {∅}} ∧ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7874, 77sylib 121 . . . . . . . 8 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐵) ∈ {∅, {∅}} ∧ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7978simprd 113 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅}))
8079adantr 274 . . . . . 6 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅}))
8164, 66, 80mpjaodan 787 . . . . 5 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
82 df-dc 820 . . . . 5 (DECID 𝑦 = {∅} ↔ (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
8381, 82sylibr 133 . . . 4 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → DECID 𝑦 = {∅})
84 simpr 109 . . . . . 6 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
8584orcd 722 . . . . 5 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
8685, 82sylibr 133 . . . 4 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → DECID 𝑦 = {∅})
87 fveq2 5414 . . . . . . . 8 (𝑧 = 𝐴 → (𝑓𝑧) = (𝑓𝐴))
88 id 19 . . . . . . . 8 (𝑧 = 𝐴𝑧 = 𝐴)
8987, 88eleq12d 2208 . . . . . . 7 (𝑧 = 𝐴 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐴) ∈ 𝐴))
906prid1 3624 . . . . . . . . 9 𝐴 ∈ {𝐴, 𝐵}
9190, 2eleqtrri 2213 . . . . . . . 8 𝐴𝐶
9291a1i 9 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐴𝐶)
9389, 70, 92rspcdva 2789 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐴) ∈ 𝐴)
94 eqeq1 2144 . . . . . . . 8 (𝑥 = (𝑓𝐴) → (𝑥 = ∅ ↔ (𝑓𝐴) = ∅))
9594orbi1d 780 . . . . . . 7 (𝑥 = (𝑓𝐴) → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9695, 3elrab2 2838 . . . . . 6 ((𝑓𝐴) ∈ 𝐴 ↔ ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9793, 96sylib 121 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9897simprd 113 . . . 4 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅}))
9983, 86, 98mpjaodan 787 . . 3 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → DECID 𝑦 = {∅})
10044, 99exlimddv 1870 . 2 ((CHOICE𝑦 ⊆ {∅}) → DECID 𝑦 = {∅})
101100exmid1dc 4118 1 (CHOICEEXMID)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 697  DECID wdc 819   = wceq 1331  wex 1468  wcel 1480  wral 2414  {crab 2418  Vcvv 2681  wss 3066  c0 3358  {csn 3522  {cpr 3523  EXMIDwem 4113   Fn wfn 5113  cfv 5118  CHOICEwac 7054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-exmid 4114  df-id 4210  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-ac 7055
This theorem is referenced by:  exmidac  7058
  Copyright terms: Public domain W3C validator