Theorem kmlem1 4745

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 groups:   x,y,φ   ψ,x   x,w,y,z

Proof of Theorem kmlem1

Step	Hyp	Ref	Expression
1		visset 1809	. . . . . 6 ⊢ v ∈ V
2	1	rabex 2720	. . . . 5 ⊢ {u ∈ v∣u ≠ ∅} ∈ V
3		raleq1 1783	. . . . . . 7 ⊢ (x = {u ∈ v∣u ≠ ∅} → (∀z ∈ x z ≠ ∅ ↔ ∀z ∈ {u ∈ v∣u ≠ ∅}z ≠ ∅))
4		raleq1 1783	. . . . . . . 8 ⊢ (x = {u ∈ v∣u ≠ ∅} → (∀w ∈ x φ ↔ ∀w ∈ {u ∈ v∣u ≠ ∅}φ))
5	4	raleqd 1788	. . . . . . 7 ⊢ (x = {u ∈ v∣u ≠ ∅} → (∀z ∈ x ∀w ∈ x φ ↔ ∀z ∈ {u ∈ v∣u ≠ ∅}∀w ∈ {u ∈ v∣u ≠ ∅}φ))
6	3, 5	anbi12d 627	. . . . . 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		raleq1 1783	. . . . . . 7 ⊢ (x = {u ∈ v∣u ≠ ∅} → (∀z ∈ x ψ ↔ ∀z ∈ {u ∈ v∣u ≠ ∅}ψ))
8	7	exbidv 1277	. . . . . 6 ⊢ (x = {u ∈ v∣u ≠ ∅} → (∃y∀z ∈ x ψ ↔ ∃y∀z ∈ {u ∈ v∣u ≠ ∅}ψ))
9	6, 8	imbi12d 625	. . . . 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 1864	. . . 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 1284	. . 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		ssrab2 2127	. . . . . . . . 9 ⊢ {u ∈ v∣u ≠ ∅} ⊆ v
13	12	sseli 2061	. . . . . . . 8 ⊢ (z ∈ {u ∈ v∣u ≠ ∅} → z ∈ v)
14	12	sseli 2061	. . . . . . . . . 10 ⊢ (w ∈ {u ∈ v∣u ≠ ∅} → w ∈ v)
15	14	imim1i 16	. . . . . . . . 9 ⊢ ((w ∈ v → φ) → (w ∈ {u ∈ v∣u ≠ ∅} → φ))
16	15	r19.20i2 1700	. . . . . . . 8 ⊢ (∀w ∈ v φ → ∀w ∈ {u ∈ v∣u ≠ ∅}φ)
17	13, 16	imim12i 18	. . . . . . 7 ⊢ ((z ∈ v → ∀w ∈ v φ) → (z ∈ {u ∈ v∣u ≠ ∅} → ∀w ∈ {u ∈ v∣u ≠ ∅}φ))
18	17	r19.20i2 1700	. . . . . 6 ⊢ (∀z ∈ v ∀w ∈ v φ → ∀z ∈ {u ∈ v∣u ≠ ∅}∀w ∈ {u ∈ v∣u ≠ ∅}φ)
19		neeq1 1587	. . . . . . . . 9 ⊢ (u = z → (u ≠ ∅ ↔ z ≠ ∅))
20	19	elrab 1901	. . . . . . . 8 ⊢ (z ∈ {u ∈ v∣u ≠ ∅} ↔ (z ∈ v ⋀ z ≠ ∅))
21	20	pm3.27bi 326	. . . . . . 7 ⊢ (z ∈ {u ∈ v∣u ≠ ∅} → z ≠ ∅)
22	21	rgen 1695	. . . . . 6 ⊢ ∀z ∈ {u ∈ v∣u ≠ ∅}z ≠ ∅
23	18, 22	jctil 292	. . . . 5 ⊢ (∀z ∈ v ∀w ∈ v φ → (∀z ∈ {u ∈ v∣u ≠ ∅}z ≠ ∅ ⋀ ∀z ∈ {u ∈ v∣u ≠ ∅}∀w ∈ {u ∈ v∣u ≠ ∅}φ))
24	20	biimpr 152	. . . . . . . . 9 ⊢ ((z ∈ v ⋀ z ≠ ∅) → z ∈ {u ∈ v∣u ≠ ∅})
25	24	imim1i 16	. . . . . . . 8 ⊢ ((z ∈ {u ∈ v∣u ≠ ∅} → ψ) → ((z ∈ v ⋀ z ≠ ∅) → ψ))
26	25	exp3a 375	. . . . . . 7 ⊢ ((z ∈ {u ∈ v∣u ≠ ∅} → ψ) → (z ∈ v → (z ≠ ∅ → ψ)))
27	26	r19.20i2 1700	. . . . . 6 ⊢ (∀z ∈ {u ∈ v∣u ≠ ∅}ψ → ∀z ∈ v (z ≠ ∅ → ψ))
28	27	19.22i 1038	. . . . 5 ⊢ (∃y∀z ∈ {u ∈ v∣u ≠ ∅}ψ → ∃y∀z ∈ v (z ≠ ∅ → ψ))
29	23, 28	imim12i 18	. . . 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 ≠ ∅ → ψ)))
30	29	19.20i 990	. . 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 ≠ ∅ → ψ)))
31	11, 30	syl 10	. 2 ⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀v(∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (z ≠ ∅ → ψ)))
32		raleq1 1783	. . . . 5 ⊢ (v = x → (∀w ∈ v φ ↔ ∀w ∈ x φ))
33	32	raleqd 1788	. . . 4 ⊢ (v = x → (∀z ∈ v ∀w ∈ v φ ↔ ∀z ∈ x ∀w ∈ x φ))
34		raleq1 1783	. . . . 5 ⊢ (v = x → (∀z ∈ v (z ≠ ∅ → ψ) ↔ ∀z ∈ x (z ≠ ∅ → ψ)))
35	34	exbidv 1277	. . . 4 ⊢ (v = x → (∃y∀z ∈ v (z ≠ ∅ → ψ) ↔ ∃y∀z ∈ x (z ≠ ∅ → ψ)))
36	33, 35	imbi12d 625	. . 3 ⊢ (v = x → ((∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (z ≠ ∅ → ψ)) ↔ (∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (z ≠ ∅ → ψ))))
37	36	cbvalv 1312	. 2 ⊢ (∀v(∀z ∈ v ∀w ∈ v φ → ∃y∀z ∈ v (z ≠ ∅ → ψ)) ↔ ∀x(∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (z ≠ ∅ → ψ)))
38	31, 37	sylib 198	1 ⊢ (∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x φ) → ∃y∀z ∈ x ψ) → ∀x(∀z ∈ x ∀w ∈ x φ → ∃y∀z ∈ x (z ≠ ∅ → ψ)))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978   ≠ wne 1582  ∀wral 1642  {crab 1645  ∅c0 2276

This theorem is referenced by:  kmlem13 4757

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rab 1649  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain