Theorem kmlem1 9837

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.)

Assertion

Ref	Expression
kmlem1	⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜓,𝑥   𝑥,𝑤,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑧,𝑤)   𝜓(𝑦,𝑧,𝑤)

Proof of Theorem kmlem1

Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3426	. . . . . 6 ⊢ 𝑣 ∈ V
2	1	rabex 5251	. . . . 5 ⊢ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ∈ V
3		raleq 3333	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅))
4		raleq 3333	. . . . . . . 8 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
5	4	raleqbi1dv 3331	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
6	3, 5	anbi12d 630	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)))
7		raleq 3333	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
8	7	exbidv 1925	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∃𝑦∀𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)))
10	2, 9	spcv 3534	. . . 4 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
11	10	alrimiv 1931	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
12		elrabi 3611	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ∈ 𝑣)
13		elrabi 3611	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑤 ∈ 𝑣)
14	13	imim1i 63	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑣 → 𝜑) → (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜑))
15	14	ralimi2 3083	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑣 𝜑 → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
16	12, 15	imim12i 62	. . . . . 6 ⊢ ((𝑧 ∈ 𝑣 → ∀𝑤 ∈ 𝑣 𝜑) → (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
17	16	ralimi2 3083	. . . . 5 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
18		neeq1 3005	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
19	18	elrab 3617	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ↔ (𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅))
20	19	simprbi 496	. . . . . 6 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ≠ ∅)
21	20	rgen 3073	. . . . 5 ⊢ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅
22	17, 21	jctil 519	. . . 4 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
23	19	biimpri 227	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅})
24	23	imim1i 63	. . . . . . 7 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝜓))
25	24	expd 415	. . . . . 6 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → (𝑧 ∈ 𝑣 → (𝑧 ≠ ∅ → 𝜓)))
26	25	ralimi2 3083	. . . . 5 ⊢ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
27	26	eximi 1838	. . . 4 ⊢ (∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
28	22, 27	imim12i 62	. . 3 ⊢ (((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
29	11, 28	sylg 1826	. 2 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
30		raleq 3333	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑤 ∈ 𝑥 𝜑))
31	30	raleqbi1dv 3331	. . . 4 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑))
32		raleq 3333	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
33	32	exbidv 1925	. . . 4 ⊢ (𝑣 = 𝑥 → (∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
34	31, 33	imbi12d 344	. . 3 ⊢ (𝑣 = 𝑥 → ((∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))))
35	34	cbvalvw 2040	. 2 ⊢ (∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
36	29, 35	sylib 217	1 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  {crab 3067  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  kmlem13  9849