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

Step	Hyp	Ref	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)))
3	1, 2	bitr2i 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}
5	4	eleq2i 2101	. . . . . . . 8 ⊢ (z ∈ 𝐶 ↔ z ∈ {A, B})
6		vex 2554	. . . . . . . . 9 ⊢ z ∈ V
7	6	elpr 3385	. . . . . . . 8 ⊢ (z ∈ {A, B} ↔ (z = A ∨ z = B))
8	5, 7	bitri 173	. . . . . . 7 ⊢ (z ∈ 𝐶 ↔ (z = A ∨ z = B))
9		onsucelsucexmidlem1 4213	. . . . . . . . . . 11 ⊢ ∅ ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
10		acexmidlem.a	. . . . . . . . . . 11 ⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
11	9, 10	eleqtrri 2110	. . . . . . . . . 10 ⊢ ∅ ∈ A
12		elex2 2564	. . . . . . . . . 10 ⊢ (∅ ∈ A → ∃w w ∈ A)
13	11, 12	ax-mp 7	. . . . . . . . 9 ⊢ ∃w w ∈ A
14		eleq2 2098	. . . . . . . . . 10 ⊢ (z = A → (w ∈ z ↔ w ∈ A))
15	14	exbidv 1703	. . . . . . . . 9 ⊢ (z = A → (∃w w ∈ z ↔ ∃w w ∈ A))
16	13, 15	mpbiri 157	. . . . . . . 8 ⊢ (z = A → ∃w w ∈ z)
17		p0ex 3930	. . . . . . . . . . . . 13 ⊢ {∅} ∈ V
18	17	prid2 3468	. . . . . . . . . . . 12 ⊢ {∅} ∈ {∅, {∅}}
19		eqid 2037	. . . . . . . . . . . . 13 ⊢ {∅} = {∅}
20	19	orci 649	. . . . . . . . . . . 12 ⊢ ({∅} = {∅} ∨ φ)
21		eqeq1 2043	. . . . . . . . . . . . . 14 ⊢ (x = {∅} → (x = {∅} ↔ {∅} = {∅}))
22	21	orbi1d 704	. . . . . . . . . . . . 13 ⊢ (x = {∅} → ((x = {∅} ∨ φ) ↔ ({∅} = {∅} ∨ φ)))
23	22	elrab 2692	. . . . . . . . . . . 12 ⊢ ({∅} ∈ {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)} ↔ ({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅} ∨ φ)))
24	18, 20, 23	mpbir2an 848	. . . . . . . . . . 11 ⊢ {∅} ∈ {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}
25		acexmidlem.b	. . . . . . . . . . 11 ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}
26	24, 25	eleqtrri 2110	. . . . . . . . . 10 ⊢ {∅} ∈ B
27		elex2 2564	. . . . . . . . . 10 ⊢ ({∅} ∈ B → ∃w w ∈ B)
28	26, 27	ax-mp 7	. . . . . . . . 9 ⊢ ∃w w ∈ B
29		eleq2 2098	. . . . . . . . . 10 ⊢ (z = B → (w ∈ z ↔ w ∈ B))
30	29	exbidv 1703	. . . . . . . . 9 ⊢ (z = B → (∃w w ∈ z ↔ ∃w w ∈ B))
31	28, 30	mpbiri 157	. . . . . . . 8 ⊢ (z = B → ∃w w ∈ z)
32	16, 31	jaoi 635	. . . . . . 7 ⊢ ((z = A ∨ z = B) → ∃w w ∈ z)
33	8, 32	sylbi 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)))
35	33, 34	syl 14	. . . . 5 ⊢ (z ∈ 𝐶 → ((∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
36	35	imp 115	. . . 4 ⊢ ((z ∈ 𝐶 ∧ (∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))
37	3, 36	sylan2br 272	. . 3 ⊢ ((z ∈ 𝐶 ∧ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))
38	37	ralimiaa 2377	. 2 ⊢ (∀z ∈ 𝐶 ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → ∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))
39	10, 25, 4	acexmidlem1 5451	. 2 ⊢ (∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ ∨ ¬ φ))
40	38, 39	syl 14	1 ⊢ (∀z ∈ 𝐶 ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ ∨ ¬ φ))

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-bndl 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