Theorem kmlem1 10135

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 3459	. . . . . 6 ⊢ 𝑣 ∈ V
2	1	rabex 5311	. . . . 5 ⊢ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ∈ V
3		raleq 3320	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅))
4		raleq 3320	. . . . . . . 8 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
5	4	raleqbi1dv 3333	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
6	3, 5	anbi12d 643	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)))
7		raleq 3320	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
8	7	exbidv 1951	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∃𝑦∀𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
9	6, 8	imbi12d 347	. . . . 5 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)))
10	2, 9	spcv 3565	. . . 4 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
11	10	alrimiv 1957	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
12		elrabi 3647	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ∈ 𝑣)
13		elrabi 3647	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑤 ∈ 𝑣)
14	13	imim1i 64	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑣 → 𝜑) → (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜑))
15	14	ralimi2 3097	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑣 𝜑 → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
16	12, 15	imim12i 63	. . . . . 6 ⊢ ((𝑧 ∈ 𝑣 → ∀𝑤 ∈ 𝑣 𝜑) → (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
17	16	ralimi2 3097	. . . . 5 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
18		neeq1 3020	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
19	18	elrab 3651	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ↔ (𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅))
20	19	simprbi 502	. . . . . 6 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ≠ ∅)
21	20	rgen 3081	. . . . 5 ⊢ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅
22	17, 21	jctil 528	. . . 4 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
23	19	biimpri 231	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅})
24	23	imim1i 64	. . . . . . 7 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝜓))
25	24	expd 420	. . . . . 6 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → (𝑧 ∈ 𝑣 → (𝑧 ≠ ∅ → 𝜓)))
26	25	ralimi2 3097	. . . . 5 ⊢ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
27	26	eximi 1865	. . . 4 ⊢ (∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
28	22, 27	imim12i 63	. . 3 ⊢ (((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
29	11, 28	sylg 1853	. 2 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
30		raleq 3320	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑤 ∈ 𝑥 𝜑))
31	30	raleqbi1dv 3333	. . . 4 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑))
32		raleq 3320	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
33	32	exbidv 1951	. . . 4 ⊢ (𝑣 = 𝑥 → (∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
34	31, 33	imbi12d 347	. . 3 ⊢ (𝑣 = 𝑥 → ((∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))))
35	34	cbvalvw 2066	. 2 ⊢ (∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
36	29, 35	sylib 221	1 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923  df-pw 4565

This theorem is referenced by:  kmlem13  10147