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

Theorem acexmidlem2 5452
Description: Lemma for acexmid 5454. This builds on acexmidlem1 5451 by noting that every element of 𝐶 is inhabited.

(Note that y is not quite a function in the df-fun 4847 sense because it uses ordered pairs as described in opthreg 4234 rather than df-op 3376).

The set A is also found in onsucelsucexmidlem 4214.

(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 2305 . . . . 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 1760 . . . . 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 2101 . . . . . . . 8 (z 𝐶z {A, B})
6 vex 2554 . . . . . . . . 9 z V
76elpr 3385 . . . . . . . 8 (z {A, B} ↔ (z = A z = B))
85, 7bitri 173 . . . . . . 7 (z 𝐶 ↔ (z = A z = B))
9 onsucelsucexmidlem1 4213 . . . . . . . . . . 11 {x {∅, {∅}} ∣ (x = ∅ φ)}
10 acexmidlem.a . . . . . . . . . . 11 A = {x {∅, {∅}} ∣ (x = ∅ φ)}
119, 10eleqtrri 2110 . . . . . . . . . 10 A
12 elex2 2564 . . . . . . . . . 10 (∅ Aw w A)
1311, 12ax-mp 7 . . . . . . . . 9 w w A
14 eleq2 2098 . . . . . . . . . 10 (z = A → (w zw A))
1514exbidv 1703 . . . . . . . . 9 (z = A → (w w zw w A))
1613, 15mpbiri 157 . . . . . . . 8 (z = Aw w z)
17 p0ex 3930 . . . . . . . . . . . . 13 {∅} V
1817prid2 3468 . . . . . . . . . . . 12 {∅} {∅, {∅}}
19 eqid 2037 . . . . . . . . . . . . 13 {∅} = {∅}
2019orci 649 . . . . . . . . . . . 12 ({∅} = {∅} φ)
21 eqeq1 2043 . . . . . . . . . . . . . 14 (x = {∅} → (x = {∅} ↔ {∅} = {∅}))
2221orbi1d 704 . . . . . . . . . . . . 13 (x = {∅} → ((x = {∅} φ) ↔ ({∅} = {∅} φ)))
2322elrab 2692 . . . . . . . . . . . 12 ({∅} {x {∅, {∅}} ∣ (x = {∅} φ)} ↔ ({∅} {∅, {∅}} ({∅} = {∅} φ)))
2418, 20, 23mpbir2an 848 . . . . . . . . . . 11 {∅} {x {∅, {∅}} ∣ (x = {∅} φ)}
25 acexmidlem.b . . . . . . . . . . 11 B = {x {∅, {∅}} ∣ (x = {∅} φ)}
2624, 25eleqtrri 2110 . . . . . . . . . 10 {∅} B
27 elex2 2564 . . . . . . . . . 10 ({∅} Bw w B)
2826, 27ax-mp 7 . . . . . . . . 9 w w B
29 eleq2 2098 . . . . . . . . . 10 (z = B → (w zw B))
3029exbidv 1703 . . . . . . . . 9 (z = B → (w w zw w B))
3128, 30mpbiri 157 . . . . . . . 8 (z = Bw w z)
3216, 31jaoi 635 . . . . . . 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 2377 . 2 (z 𝐶 w z ∃!v z u y (z u v u) → z 𝐶 ∃!v z u y (z u v u))
3910, 25, 4acexmidlem1 5451 . 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 628  wal 1240   = wceq 1242  wex 1378   wcel 1390  wral 2300  wrex 2301  ∃!wreu 2302  {crab 2304  c0 3218  {csn 3367  {cpr 3368
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918
This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-uni 3572  df-tr 3846  df-iord 4069  df-on 4071  df-suc 4074  df-iota 4810  df-riota 5411
This theorem is referenced by:  acexmidlemv  5453
  Copyright terms: Public domain W3C validator