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

Theorem acexmidlem2 5433
 Description: Lemma for acexmid 5435. This builds on acexmidlem1 5432 by noting that every element of 𝐶 is inhabited. (Note that y is not quite a function in the df-fun 4831 sense because it uses ordered pairs as described in opthreg 4218 rather than df-op 3359). The set A is also found in onsucelsucexmidlem 4198. (Contributed by Jim Kingdon, 5-Aug-2019.)
Hypotheses
Ref Expression
acexmidlem.a A = {x {∅, {∅}} ∣ (x = ∅ φ)}
acexmidlem.b B = {x {∅, {∅}} ∣ (x = {∅} φ)}
acexmidlem.c 𝐶 = {A, B}
Assertion
Ref Expression
acexmidlem2 (z 𝐶 w z ∃!v z u y (z u v u) → (φ ¬ φ))
Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,𝐶,y,z,w,v,u   φ,x,y,z,w,v,u

Proof of Theorem acexmidlem2
StepHypRef Expression
1 df-ral 2289 . . . . 5 (w z ∃!v z u y (z u v u) ↔ w(w z∃!v z u y (z u v u)))
2 19.23v 1745 . . . . 5 (w(w z∃!v z u y (z u v u)) ↔ (w w z∃!v z u y (z u v u)))
31, 2bitr2i 174 . . . 4 ((w w z∃!v z u y (z u v u)) ↔ w z ∃!v z u y (z u v u))
4 acexmidlem.c . . . . . . . . 9 𝐶 = {A, B}
54eleq2i 2086 . . . . . . . 8 (z 𝐶z {A, B})
6 vex 2538 . . . . . . . . 9 z V
76elpr 3368 . . . . . . . 8 (z {A, B} ↔ (z = A z = B))
85, 7bitri 173 . . . . . . 7 (z 𝐶 ↔ (z = A z = B))
9 onsucelsucexmidlem1 4197 . . . . . . . . . . 11 {x {∅, {∅}} ∣ (x = ∅ φ)}
10 acexmidlem.a . . . . . . . . . . 11 A = {x {∅, {∅}} ∣ (x = ∅ φ)}
119, 10eleqtrri 2095 . . . . . . . . . 10 A
12 elex2 2547 . . . . . . . . . 10 (∅ Aw w A)
1311, 12ax-mp 7 . . . . . . . . 9 w w A
14 eleq2 2083 . . . . . . . . . 10 (z = A → (w zw A))
1514exbidv 1688 . . . . . . . . 9 (z = A → (w w zw w A))
1613, 15mpbiri 157 . . . . . . . 8 (z = Aw w z)
17 p0ex 3913 . . . . . . . . . . . . 13 {∅} V
1817prid2 3451 . . . . . . . . . . . 12 {∅} {∅, {∅}}
19 eqid 2022 . . . . . . . . . . . . 13 {∅} = {∅}
2019orci 637 . . . . . . . . . . . 12 ({∅} = {∅} φ)
21 eqeq1 2028 . . . . . . . . . . . . . 14 (x = {∅} → (x = {∅} ↔ {∅} = {∅}))
2221orbi1d 692 . . . . . . . . . . . . 13 (x = {∅} → ((x = {∅} φ) ↔ ({∅} = {∅} φ)))
2322elrab 2675 . . . . . . . . . . . 12 ({∅} {x {∅, {∅}} ∣ (x = {∅} φ)} ↔ ({∅} {∅, {∅}} ({∅} = {∅} φ)))
2418, 20, 23mpbir2an 837 . . . . . . . . . . 11 {∅} {x {∅, {∅}} ∣ (x = {∅} φ)}
25 acexmidlem.b . . . . . . . . . . 11 B = {x {∅, {∅}} ∣ (x = {∅} φ)}
2624, 25eleqtrri 2095 . . . . . . . . . 10 {∅} B
27 elex2 2547 . . . . . . . . . 10 ({∅} Bw w B)
2826, 27ax-mp 7 . . . . . . . . 9 w w B
29 eleq2 2083 . . . . . . . . . 10 (z = B → (w zw B))
3029exbidv 1688 . . . . . . . . 9 (z = B → (w w zw w B))
3128, 30mpbiri 157 . . . . . . . 8 (z = Bw w z)
3216, 31jaoi 623 . . . . . . 7 ((z = A z = B) → w w z)
338, 32sylbi 114 . . . . . 6 (z 𝐶w w z)
34 pm2.27 35 . . . . . 6 (w w z → ((w w z∃!v z u y (z u v u)) → ∃!v z u y (z u v u)))
3533, 34syl 14 . . . . 5 (z 𝐶 → ((w w z∃!v z u y (z u v u)) → ∃!v z u y (z u v u)))
3635imp 115 . . . 4 ((z 𝐶 (w w z∃!v z u y (z u v u))) → ∃!v z u y (z u v u))
373, 36sylan2br 272 . . 3 ((z 𝐶 w z ∃!v z u y (z u v u)) → ∃!v z u y (z u v u))
3837ralimiaa 2361 . 2 (z 𝐶 w z ∃!v z u y (z u v u) → z 𝐶 ∃!v z u y (z u v u))
3910, 25, 4acexmidlem1 5432 . 2 (z 𝐶 ∃!v z u y (z u v u) → (φ ¬ φ))
4038, 39syl 14 1 (z 𝐶 w z ∃!v z u y (z u v u) → (φ ¬ φ))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 616  ∀wal 1226   = wceq 1228  ∃wex 1362   ∈ wcel 1374  ∀wral 2284  ∃wrex 2285  ∃!wreu 2286  {crab 2288  ∅c0 3201  {csn 3350  {cpr 3351 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 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-nul 3857  ax-pow 3901 This theorem depends on definitions:  df-bi 110  df-3or 874  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-uni 3555  df-tr 3829  df-iord 4052  df-on 4054  df-suc 4057  df-iota 4794  df-riota 5393 This theorem is referenced by:  acexmidlemv  5434
 Copyright terms: Public domain W3C validator