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

Step	Hyp	Ref	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)))
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 2086	. . . . . . . 8 ⊢ (z ∈ 𝐶 ↔ z ∈ {A, B})
6		vex 2538	. . . . . . . . 9 ⊢ z ∈ V
7	6	elpr 3368	. . . . . . . 8 ⊢ (z ∈ {A, B} ↔ (z = A ∨ z = B))
8	5, 7	bitri 173	. . . . . . 7 ⊢ (z ∈ 𝐶 ↔ (z = A ∨ z = B))
9		onsucelsucexmidlem1 4197	. . . . . . . . . . 11 ⊢ ∅ ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
10		acexmidlem.a	. . . . . . . . . . 11 ⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
11	9, 10	eleqtrri 2095	. . . . . . . . . 10 ⊢ ∅ ∈ A
12		elex2 2547	. . . . . . . . . 10 ⊢ (∅ ∈ A → ∃w w ∈ A)
13	11, 12	ax-mp 7	. . . . . . . . 9 ⊢ ∃w w ∈ A
14		eleq2 2083	. . . . . . . . . 10 ⊢ (z = A → (w ∈ z ↔ w ∈ A))
15	14	exbidv 1688	. . . . . . . . 9 ⊢ (z = A → (∃w w ∈ z ↔ ∃w w ∈ A))
16	13, 15	mpbiri 157	. . . . . . . 8 ⊢ (z = A → ∃w w ∈ z)
17		p0ex 3913	. . . . . . . . . . . . 13 ⊢ {∅} ∈ V
18	17	prid2 3451	. . . . . . . . . . . 12 ⊢ {∅} ∈ {∅, {∅}}
19		eqid 2022	. . . . . . . . . . . . 13 ⊢ {∅} = {∅}
20	19	orci 637	. . . . . . . . . . . 12 ⊢ ({∅} = {∅} ∨ φ)
21		eqeq1 2028	. . . . . . . . . . . . . 14 ⊢ (x = {∅} → (x = {∅} ↔ {∅} = {∅}))
22	21	orbi1d 692	. . . . . . . . . . . . 13 ⊢ (x = {∅} → ((x = {∅} ∨ φ) ↔ ({∅} = {∅} ∨ φ)))
23	22	elrab 2675	. . . . . . . . . . . 12 ⊢ ({∅} ∈ {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)} ↔ ({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅} ∨ φ)))
24	18, 20, 23	mpbir2an 837	. . . . . . . . . . 11 ⊢ {∅} ∈ {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}
25		acexmidlem.b	. . . . . . . . . . 11 ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}
26	24, 25	eleqtrri 2095	. . . . . . . . . 10 ⊢ {∅} ∈ B
27		elex2 2547	. . . . . . . . . 10 ⊢ ({∅} ∈ B → ∃w w ∈ B)
28	26, 27	ax-mp 7	. . . . . . . . 9 ⊢ ∃w w ∈ B
29		eleq2 2083	. . . . . . . . . 10 ⊢ (z = B → (w ∈ z ↔ w ∈ B))
30	29	exbidv 1688	. . . . . . . . 9 ⊢ (z = B → (∃w w ∈ z ↔ ∃w w ∈ B))
31	28, 30	mpbiri 157	. . . . . . . 8 ⊢ (z = B → ∃w w ∈ z)
32	16, 31	jaoi 623	. . . . . . 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 2361	. 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 5432	. 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 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