Theorem kmlem1 3580

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2.

Assertion

Ref	Expression
kmlem1	⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀x(∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (¬ z = ∅ → ψ)))

Distinct variable group(s):   x,y,z,w   φ,x,y   ψ,x

Proof of Theorem kmlem1

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 ⊢ v ∈ V
2	1	rabex 1706	. . . . 5 ⊢ {u ∈ v∣ ¬ u = ∅} ∈ V
3		raleq 1324	. . . . . . 7 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (∀z ∈ x ¬ z = ∅ ↔ ∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅))
4		raleq 1324	. . . . . . . 8 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (∀w ∈ x φ ↔ ∀w ∈ {u ∈ v∣ ¬ u = ∅}φ))
5	4	raleqd 1327	. . . . . . 7 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (∀z ∈ x ∀w ∈ x φ ↔ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ))
6	3, 5	anbi12d 476	. . . . . 6 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → ((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) ↔ (∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ)))
7		raleq 1324	. . . . . . 7 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (∀z ∈ x ψ ↔ ∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ))
8	7	biexdv 936	. . . . . 6 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (∃y∀z ∈ x ψ ↔ ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ))
9	6, 8	imbi12d 474	. . . . 5 ⊢ (x = {u ∈ v∣ ¬ u = ∅} → (((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) ↔ ((∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ) → ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ)))
10	2, 9	cla4v 1400	. . . 4 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ((∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ) → ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ))
11	10	19.21aiv 943	. . 3 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀v((∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ) → ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ))
12		ssrab 1556	. . . . . . . . 9 ⊢ {u ∈ v∣ ¬ u = ∅} ⊆ v
13	12	sseli 1504	. . . . . . . 8 ⊢ (z ∈ {u ∈ v∣ ¬ u = ∅} → z ∈ v)
14	12	sseli 1504	. . . . . . . . . 10 ⊢ (w ∈ {u ∈ v∣ ¬ u = ∅} → w ∈ v)
15	14	syl4 19	. . . . . . . . 9 ⊢ ((w ∈ v → φ) → (w ∈ {u ∈ v∣ ¬ u = ∅} → φ))
16	15	r19.20i2 1252	. . . . . . . 8 ⊢ (∀w ∈ v φ → ∀w ∈ {u ∈ v∣ ¬ u = ∅}φ)
17	13, 16	syl34 20	. . . . . . 7 ⊢ ((z ∈ v → ∀w ∈ v φ) → (z ∈ {u ∈ v∣ ¬ u = ∅} → ∀w ∈ {u ∈ v∣ ¬ u = ∅}φ))
18	17	r19.20i2 1252	. . . . . 6 ⊢ (∀z ∈ v ∀w ∈ v φ → ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ)
19		cleq1 1107	. . . . . . . . . 10 ⊢ (u = z → (u = ∅ ↔ z = ∅))
20	19	negbid 463	. . . . . . . . 9 ⊢ (u = z → (¬ u = ∅ ↔ ¬ z = ∅))
21	20	elrab 1422	. . . . . . . 8 ⊢ (z ∈ {u ∈ v∣ ¬ u = ∅} ↔ (z ∈ v ∧ ¬ z = ∅))
22	21	pm3.27bd 263	. . . . . . 7 ⊢ (z ∈ {u ∈ v∣ ¬ u = ∅} → ¬ z = ∅)
23	22	rgen 1247	. . . . . 6 ⊢ ∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅
24	18, 23	jctil 240	. . . . 5 ⊢ (∀z ∈ v ∀w ∈ v φ → (∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ))
25	21	biimpr 134	. . . . . . . . 9 ⊢ ((z ∈ v ∧ ¬ z = ∅) → z ∈ {u ∈ v∣ ¬ u = ∅})
26	25	syl4 19	. . . . . . . 8 ⊢ ((z ∈ {u ∈ v∣ ¬ u = ∅} → ψ) → ((z ∈ v ∧ ¬ z = ∅) → ψ))
27	26	exp3a 292	. . . . . . 7 ⊢ ((z ∈ {u ∈ v∣ ¬ u = ∅} → ψ) → (z ∈ v → (¬ z = ∅ → ψ)))
28	27	r19.20i2 1252	. . . . . 6 ⊢ (∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ → ∀z ∈ v (¬ z = ∅ → ψ))
29	28	19.22i 723	. . . . 5 ⊢ (∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ → ∃y∀z ∈ v (¬ z = ∅ → ψ))
30	24, 29	syl34 20	. . . 4 ⊢ (((∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ) → ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ) → (∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (¬ z = ∅ → ψ)))
31	30	19.20i 691	. . 3 ⊢ (∀v((∀z ∈ {u ∈ v∣ ¬ u = ∅} ¬ z = ∅ ∧ ∀z ∈ {u ∈ v∣ ¬ u = ∅}∀w ∈ {u ∈ v∣ ¬ u = ∅}φ) → ∃y∀z ∈ {u ∈ v∣ ¬ u = ∅}ψ) → ∀v(∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (¬ z = ∅ → ψ)))
32	11, 31	syl 12	. 2 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀v(∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (¬ z = ∅ → ψ)))
33		raleq 1324	. . . . 5 ⊢ (v = x → (∀w ∈ v φ ↔ ∀w ∈ x φ))
34	33	raleqd 1327	. . . 4 ⊢ (v = x → (∀z ∈ v ∀w ∈ v φ ↔ ∀z ∈ x ∀w ∈ x φ))
35		raleq 1324	. . . . 5 ⊢ (v = x → (∀z ∈ v (¬ z = ∅ → ψ) ↔ ∀z ∈ x (¬ z = ∅ → ψ)))
36	35	biexdv 936	. . . 4 ⊢ (v = x → (∃y∀z ∈ v (¬ z = ∅ → ψ) ↔ ∃y∀z ∈ x (¬ z = ∅ → ψ)))
37	34, 36	imbi12d 474	. . 3 ⊢ (v = x → ((∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (¬ z = ∅ → ψ)) ↔ (∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (¬ z = ∅ → ψ))))
38	37	cbvalv 972	. 2 ⊢ (∀v(∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (¬ z = ∅ → ψ)) ↔ ∀x(∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (¬ z = ∅ → ψ)))
39	32, 38	sylib 173	1 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀x(∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (¬ z = ∅ → ψ)))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  {crab 1204  ∅c0 1707

This theorem is referenced by:  kmlem12 3591

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rab 1208  df-v 1349  df-in 1491  df-ss 1492

metamath.org