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

Theorem exmidaclem 7197
Description: Lemma for exmidac 7198. 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 4184 . . . . . . . . 9 {∅, {∅}} ∈ V
54rabex 4142 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ∈ V
63, 5eqeltri 2248 . . . . . . 7 𝐴 ∈ V
7 exmidaclem.b . . . . . . . 8 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}
84rabex 4142 . . . . . . . 8 {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ∈ V
97, 8eqeltri 2248 . . . . . . 7 𝐵 ∈ V
10 prexg 4205 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
116, 9, 10mp2an 426 . . . . . 6 {𝐴, 𝐵} ∈ V
122, 11eqeltri 2248 . . . . 5 𝐶 ∈ V
1312a1i 9 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → 𝐶 ∈ V)
14 simpr 110 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧𝐶)
1514, 2eleqtrdi 2268 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → 𝑧 ∈ {𝐴, 𝐵})
16 elpri 3612 . . . . . 6 (𝑧 ∈ {𝐴, 𝐵} → (𝑧 = 𝐴𝑧 = 𝐵))
17 0ex 4125 . . . . . . . . . . 11 ∅ ∈ V
1817prid1 3695 . . . . . . . . . 10 ∅ ∈ {∅, {∅}}
19 eqid 2175 . . . . . . . . . . 11 ∅ = ∅
2019orci 731 . . . . . . . . . 10 (∅ = ∅ ∨ 𝑦 = {∅})
21 eqeq1 2182 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ = ∅))
2221orbi1d 791 . . . . . . . . . . 11 (𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ (∅ = ∅ ∨ 𝑦 = {∅})))
2322, 3elrab2 2894 . . . . . . . . . 10 (∅ ∈ 𝐴 ↔ (∅ ∈ {∅, {∅}} ∧ (∅ = ∅ ∨ 𝑦 = {∅})))
2418, 20, 23mpbir2an 942 . . . . . . . . 9 ∅ ∈ 𝐴
25 eleq2 2239 . . . . . . . . 9 (𝑧 = 𝐴 → (∅ ∈ 𝑧 ↔ ∅ ∈ 𝐴))
2624, 25mpbiri 168 . . . . . . . 8 (𝑧 = 𝐴 → ∅ ∈ 𝑧)
27 elex2 2751 . . . . . . . 8 (∅ ∈ 𝑧 → ∃𝑤 𝑤𝑧)
2826, 27syl 14 . . . . . . 7 (𝑧 = 𝐴 → ∃𝑤 𝑤𝑧)
29 p0ex 4183 . . . . . . . . . . 11 {∅} ∈ V
3029prid2 3696 . . . . . . . . . 10 {∅} ∈ {∅, {∅}}
31 eqid 2175 . . . . . . . . . . 11 {∅} = {∅}
3231orci 731 . . . . . . . . . 10 ({∅} = {∅} ∨ 𝑦 = {∅})
33 eqeq1 2182 . . . . . . . . . . . 12 (𝑥 = {∅} → (𝑥 = {∅} ↔ {∅} = {∅}))
3433orbi1d 791 . . . . . . . . . . 11 (𝑥 = {∅} → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ({∅} = {∅} ∨ 𝑦 = {∅})))
3534, 7elrab2 2894 . . . . . . . . . 10 ({∅} ∈ 𝐵 ↔ ({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅} ∨ 𝑦 = {∅})))
3630, 32, 35mpbir2an 942 . . . . . . . . 9 {∅} ∈ 𝐵
37 eleq2 2239 . . . . . . . . 9 (𝑧 = 𝐵 → ({∅} ∈ 𝑧 ↔ {∅} ∈ 𝐵))
3836, 37mpbiri 168 . . . . . . . 8 (𝑧 = 𝐵 → {∅} ∈ 𝑧)
39 elex2 2751 . . . . . . . 8 ({∅} ∈ 𝑧 → ∃𝑤 𝑤𝑧)
4038, 39syl 14 . . . . . . 7 (𝑧 = 𝐵 → ∃𝑤 𝑤𝑧)
4128, 40jaoi 716 . . . . . 6 ((𝑧 = 𝐴𝑧 = 𝐵) → ∃𝑤 𝑤𝑧)
4215, 16, 413syl 17 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ 𝑧𝐶) → ∃𝑤 𝑤𝑧)
4342ralrimiva 2548 . . . 4 ((CHOICE𝑦 ⊆ {∅}) → ∀𝑧𝐶𝑤 𝑤𝑧)
441, 13, 43acfun 7196 . . 3 ((CHOICE𝑦 ⊆ {∅}) → ∃𝑓(𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧))
45 0nep0 4160 . . . . . . . . . 10 ∅ ≠ {∅}
4645neii 2347 . . . . . . . . 9 ¬ ∅ = {∅}
47 simplr 528 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐴) = ∅)
48 simpr 110 . . . . . . . . . 10 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → (𝑓𝐵) = {∅})
4947, 48eqeq12d 2190 . . . . . . . . 9 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ((𝑓𝐴) = (𝑓𝐵) ↔ ∅ = {∅}))
5046, 49mtbiri 675 . . . . . . . 8 (((((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) ∧ (𝑓𝐴) = ∅) ∧ (𝑓𝐵) = {∅}) → ¬ (𝑓𝐴) = (𝑓𝐵))
51 olc 711 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = ∅ ∨ 𝑦 = {∅}))
5251ralrimivw 2549 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
53 rabid2 2651 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = ∅ ∨ 𝑦 = {∅}))
5452, 53sylibr 134 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})})
5554, 3eqtr4di 2226 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐴)
56 olc 711 . . . . . . . . . . . . 13 (𝑦 = {∅} → (𝑥 = {∅} ∨ 𝑦 = {∅}))
5756ralrimivw 2549 . . . . . . . . . . . 12 (𝑦 = {∅} → ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
58 rabid2 2651 . . . . . . . . . . . 12 ({∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} ↔ ∀𝑥 ∈ {∅, {∅}} (𝑥 = {∅} ∨ 𝑦 = {∅}))
5957, 58sylibr 134 . . . . . . . . . . 11 (𝑦 = {∅} → {∅, {∅}} = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})})
6059, 7eqtr4di 2226 . . . . . . . . . 10 (𝑦 = {∅} → {∅, {∅}} = 𝐵)
6155, 60eqtr3d 2210 . . . . . . . . 9 (𝑦 = {∅} → 𝐴 = 𝐵)
6261fveq2d 5511 . . . . . . . 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 5507 . . . . . . . . . . 11 (𝑧 = 𝐵 → (𝑓𝑧) = (𝑓𝐵))
68 id 19 . . . . . . . . . . 11 (𝑧 = 𝐵𝑧 = 𝐵)
6967, 68eleq12d 2246 . . . . . . . . . 10 (𝑧 = 𝐵 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐵) ∈ 𝐵))
70 simprr 531 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)
719prid2 3696 . . . . . . . . . . . 12 𝐵 ∈ {𝐴, 𝐵}
7271, 2eleqtrri 2251 . . . . . . . . . . 11 𝐵𝐶
7372a1i 9 . . . . . . . . . 10 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐵𝐶)
7469, 70, 73rspcdva 2844 . . . . . . . . 9 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐵) ∈ 𝐵)
75 eqeq1 2182 . . . . . . . . . . 11 (𝑥 = (𝑓𝐵) → (𝑥 = {∅} ↔ (𝑓𝐵) = {∅}))
7675orbi1d 791 . . . . . . . . . 10 (𝑥 = (𝑓𝐵) → ((𝑥 = {∅} ∨ 𝑦 = {∅}) ↔ ((𝑓𝐵) = {∅} ∨ 𝑦 = {∅})))
7776, 7elrab2 2894 . . . . . . . . 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 5507 . . . . . . . 8 (𝑧 = 𝐴 → (𝑓𝑧) = (𝑓𝐴))
88 id 19 . . . . . . . 8 (𝑧 = 𝐴𝑧 = 𝐴)
8987, 88eleq12d 2246 . . . . . . 7 (𝑧 = 𝐴 → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓𝐴) ∈ 𝐴))
906prid1 3695 . . . . . . . . 9 𝐴 ∈ {𝐴, 𝐵}
9190, 2eleqtrri 2251 . . . . . . . 8 𝐴𝐶
9291a1i 9 . . . . . . 7 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → 𝐴𝐶)
9389, 70, 92rspcdva 2844 . . . . . 6 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → (𝑓𝐴) ∈ 𝐴)
94 eqeq1 2182 . . . . . . . 8 (𝑥 = (𝑓𝐴) → (𝑥 = ∅ ↔ (𝑓𝐴) = ∅))
9594orbi1d 791 . . . . . . 7 (𝑥 = (𝑓𝐴) → ((𝑥 = ∅ ∨ 𝑦 = {∅}) ↔ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9695, 3elrab2 2894 . . . . . 6 ((𝑓𝐴) ∈ 𝐴 ↔ ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9793, 96sylib 122 . . . . 5 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) ∈ {∅, {∅}} ∧ ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅})))
9897simprd 114 . . . 4 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → ((𝑓𝐴) = ∅ ∨ 𝑦 = {∅}))
9983, 86, 98mpjaodan 798 . . 3 (((CHOICE𝑦 ⊆ {∅}) ∧ (𝑓 Fn 𝐶 ∧ ∀𝑧𝐶 (𝑓𝑧) ∈ 𝑧)) → DECID 𝑦 = {∅})
10044, 99exlimddv 1896 . 2 ((CHOICE𝑦 ⊆ {∅}) → DECID 𝑦 = {∅})
101100exmid1dc 4195 1 (CHOICEEXMID)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 708  DECID wdc 834   = wceq 1353  wex 1490  wcel 2146  wral 2453  {crab 2457  Vcvv 2735  wss 3127  c0 3420  {csn 3589  {cpr 3590  EXMIDwem 4189   Fn wfn 5203  cfv 5208  CHOICEwac 7194
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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-exmid 4190  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-ac 7195
This theorem is referenced by:  exmidac  7198
  Copyright terms: Public domain W3C validator