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

Theorem exmidaclem 7201
Description: Lemma for exmidac 7202. 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 109 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → CHOICE)
2 exmidaclem.c . . . . . 6 𝐶 = {𝐴, 𝐵}
3 exmidaclem.a . . . . . . . 8 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}
4 pp0ex 4186 . . . . . . . . 9 {∅, {∅}} ∈ V
54rabex 4144 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ∈ V
63, 5eqeltri 2250 . . . . . . 7 𝐴 ∈ V
7 exmidaclem.b . . . . . . . 8 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}
84rabex 4144 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ∈ V
97, 8eqeltri 2250 . . . . . . 7 𝐵 ∈ V
10 prexg 4208 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
116, 9, 10mp2an 426 . . . . . 6 {𝐴, 𝐵} ∈ V
122, 11eqeltri 2250 . . . . 5 𝐶 ∈ V
1312a1i 9 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → 𝐶 ∈ V)
14 simpr 110 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧𝐶)
1514, 2eleqtrdi 2270 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧 ∈ {𝐴, 𝐵})
16 elpri 3614 . . . . . 6 (𝑧 ∈ {𝐴, 𝐵} → (𝑧 = 𝐴𝑧 = 𝐵))
17 0ex 4127 . . . . . . . . . . 11 ∅ ∈ V
1817prid1 3697 . . . . . . . . . 10 ∅ ∈ {∅, {∅}}
19 eqid 2177 . . . . . . . . . . 11 ∅ = ∅
2019orci 731 . . . . . . . . . 10 (∅ = ∅ ∨ 𝑦 = {∅})
21 eqeq1 2184 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ = ∅))
2221orbi1d 791 . . . . . . . . . . 11 (𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ (∅ = ∅ ∨ 𝑦 = {∅})))
2322, 3elrab2 2896 . . . . . . . . . 10 (∅ ∈ 𝐴 ↔ (∅ ∈ {∅, {∅}} ∧ (∅ = ∅ ∨ 𝑦 = {∅})))
2418, 20, 23mpbir2an 942 . . . . . . . . 9 ∅ ∈ 𝐴
25 eleq2 2241 . . . . . . . . 9 (𝑧 = 𝐴 → (∅ ∈ 𝑧 ↔ ∅ ∈ 𝐴))
2624, 25mpbiri 168 . . . . . . . 8 (𝑧 = 𝐴 → ∅ ∈ 𝑧)
27 elex2 2753 . . . . . . . 8 (∅ ∈ 𝑧 → ∃𝑤 𝑤𝑧)
2826, 27syl 14 . . . . . . 7 (𝑧 = 𝐴 → ∃𝑤 𝑤𝑧)
29 p0ex 4185 . . . . . . . . . . 11 {∅} ∈ V
3029prid2 3698 . . . . . . . . . 10 {∅} ∈ {∅, {∅}}
31 eqid 2177 . . . . . . . . . . 11 {∅} = {∅}
3231orci 731 . . . . . . . . . 10 ({∅} = {∅} ∨ 𝑦 = {∅})
33 eqeq1 2184 . . . . . . . . . . . 12 (𝑥 = {∅} → (𝑥 = {∅} ↔ {∅} = {∅}))
3433orbi1d 791 . . . . . . . . . . 11 (𝑥 = {∅} → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ({∅} = {∅} ∨ 𝑦 = {∅})))
3534, 7elrab2 2896 . . . . . . . . . 10 ({∅} ∈ 𝐵 ↔ ({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅} ∨ 𝑦 = {∅})))
3630, 32, 35mpbir2an 942 . . . . . . . . 9 {∅} ∈ 𝐵
37 eleq2 2241 . . . . . . . . 9 (𝑧 = 𝐵 → ({∅} ∈ 𝑧 ↔ {∅} ∈ 𝐵))
3836, 37mpbiri 168 . . . . . . . 8 (𝑧 = 𝐵 → {∅} ∈ 𝑧)
39 elex2 2753 . . . . . . . 8 ({∅} ∈ 𝑧 → ∃𝑤 𝑤𝑧)
4038, 39syl 14 . . . . . . 7 (𝑧 = 𝐵 → ∃𝑤 𝑤𝑧)
4128, 40jaoi 716 . . . . . 6 ((𝑧 = 𝐴𝑧 = 𝐵) → ∃𝑤 𝑤𝑧)
4215, 16, 413syl 17 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → ∃𝑤 𝑤𝑧)
4342ralrimiva 2550 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → ∀𝑧𝐶𝑤 𝑤𝑧)
441, 13, 43acfun 7200 . . 3 ((CHOICE𝑦 ⊆ {∅}) → ∃𝑓(𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧))
45 0nep0 4162 . . . . . . . . . 10 ∅ ≠ {∅}
4645neii 2349 . . . . . . . . 9 ¬ ∅ = {∅}
47 simplr 528 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐴) = ∅)
48 simpr 110 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐵) = {∅})
4947, 48eqeq12d 2192 . . . . . . . . 9 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ((𝑓𝐴) = (𝑓𝐵) ↔ ∅ = {∅}))
5046, 49mtbiri 675 . . . . . . . 8 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ¬ (𝑓𝐴) = (𝑓𝐵))
51 olc 711 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = ∅ ∨ 𝑦 = {∅}))
5251ralrimivw 2551 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
53 rabid2 2653 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
5452, 53sylibr 134 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})})
5554, 3eqtr4di 2228 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐴)
56 olc 711 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = {∅} ∨ 𝑦 = {∅}))
5756ralrimivw 2551 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
58 rabid2 2653 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
5957, 58sylibr 134 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})})
6059, 7eqtr4di 2228 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐵)
6155, 60eqtr3d 2212 . . . . . . . . 9 (𝑦 = {∅} → 𝐴 = 𝐵)
6261fveq2d 5515 . . . . . . . 8 (𝑦 = {∅} → (𝑓𝐴) = (𝑓𝐵))
6350, 62nsyl 628 . . . . . . 7 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ¬ 𝑦 = {∅})
6463olcd 734 . . . . . 6 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
65 simpr 110 . . . . . . 7 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
6665orcd 733 . . . . . 6 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ 𝑦 = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
67 fveq2 5511 . . . . . . . . . . 11 (𝑧 = 𝐵 → (𝑓𝑧) = (𝑓𝐵))
68 id 19 . . . . . . . . . . 11 (𝑧 = 𝐵𝑧 = 𝐵)
6967, 68eleq12d 2248 . . . . . . . . . 10 (𝑧 = 𝐵 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐵) ∈ 𝐵))
70 simprr 531 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)
719prid2 3698 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
7271, 2eleqtrri 2253 . . . . . . . . . . 11 𝐵𝐶
7372a1i 9 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐵𝐶)
7469, 70, 73rspcdva 2846 . . . . . . . . 9 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐵) ∈ 𝐵)
75 eqeq1 2184 . . . . . . . . . . 11 (𝑥 = (𝑓𝐵) → (𝑥 = {∅} ↔ (𝑓𝐵) = {∅}))
7675orbi1d 791 . . . . . . . . . 10 (𝑥 = (𝑓𝐵) → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7776, 7elrab2 2896 . . . . . . . . 9 ((𝑓𝐵) ∈ 𝐵 ↔ ((𝑓𝐵) ∈ {∅, {∅}} ∧ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7874, 77sylib 122 . . . . . . . 8 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐵) ∈ {∅, {∅}} ∧ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7978simprd 114 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅}))
8079adantr 276 . . . . . 6 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅}))
8164, 66, 80mpjaodan 798 . . . . 5 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
82 df-dc 835 . . . . 5 (DECID 𝑦 = {∅} ↔ (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
8381, 82sylibr 134 . . . 4 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) → DECID 𝑦 = {∅})
84 simpr 110 . . . . . 6 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
8584orcd 733 . . . . 5 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → (𝑦 = {∅} ∨ ¬ 𝑦 = {∅}))
8685, 82sylibr 134 . . . 4 ((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ 𝑦 = {∅}) → DECID 𝑦 = {∅})
87 fveq2 5511 . . . . . . . 8 (𝑧 = 𝐴 → (𝑓𝑧) = (𝑓𝐴))
88 id 19 . . . . . . . 8 (𝑧 = 𝐴𝑧 = 𝐴)
8987, 88eleq12d 2248 . . . . . . 7 (𝑧 = 𝐴 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐴) ∈ 𝐴))
906prid1 3697 . . . . . . . . 9 𝐴 ∈ {𝐴, 𝐵}
9190, 2eleqtrri 2253 . . . . . . . 8 𝐴𝐶
9291a1i 9 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐴𝐶)
9389, 70, 92rspcdva 2846 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐴) ∈ 𝐴)
94 eqeq1 2184 . . . . . . . 8 (𝑥 = (𝑓𝐴) → (𝑥 = ∅ ↔ (𝑓𝐴) = ∅))
9594orbi1d 791 . . . . . . 7 (𝑥 = (𝑓𝐴) → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9695, 3elrab2 2896 . . . . . 6 ((𝑓𝐴) ∈ 𝐴 ↔ ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9793, 96sylib 122 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9897simprd 114 . . . 4 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅}))
9983, 86, 98mpjaodan 798 . . 3 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → DECID 𝑦 = {∅})
10044, 99exlimddv 1898 . 2 ((CHOICE𝑦 ⊆ {∅}) → DECID 𝑦 = {∅})
101100exmid1dc 4197 1 (CHOICEEXMID)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 708  DECID wdc 834   = wceq 1353  wex 1492  wcel 2148  wral 2455  {crab 2459  Vcvv 2737  wss 3129  c0 3422  {csn 3591  {cpr 3592  EXMIDwem 4191   Fn wfn 5207  cfv 5212  CHOICEwac 7198
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 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430
This theorem depends on definitions:  df-bi 117  df-dc 835  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-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-exmid 4192  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ac 7199
This theorem is referenced by:  exmidac  7202
  Copyright terms: Public domain W3C validator