Theorem kmlem1 10153

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 3462	. . . . . 6 ⊢ 𝑣 ∈ V
2	1	rabex 5314	. . . . 5 ⊢ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ∈ V
3		raleq 3323	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅))
4		raleq 3323	. . . . . . . 8 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
5	4	raleqbi1dv 3336	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
6	3, 5	anbi12d 644	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)))
7		raleq 3323	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
8	7	exbidv 1954	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∃𝑦∀𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
9	6, 8	imbi12d 347	. . . . 5 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)))
10	2, 9	spcv 3567	. . . 4 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
11	10	alrimiv 1960	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
12		elrabi 3649	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ∈ 𝑣)
13		elrabi 3649	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑤 ∈ 𝑣)
14	13	imim1i 64	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑣 → 𝜑) → (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜑))
15	14	ralimi2 3100	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑣 𝜑 → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
16	12, 15	imim12i 63	. . . . . 6 ⊢ ((𝑧 ∈ 𝑣 → ∀𝑤 ∈ 𝑣 𝜑) → (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
17	16	ralimi2 3100	. . . . 5 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
18		neeq1 3023	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
19	18	elrab 3653	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ↔ (𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅))
20	19	simprbi 503	. . . . . 6 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ≠ ∅)
21	20	rgen 3084	. . . . 5 ⊢ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅
22	17, 21	jctil 529	. . . 4 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
23	19	biimpri 231	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅})
24	23	imim1i 64	. . . . . . 7 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝜓))
25	24	expd 421	. . . . . 6 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → (𝑧 ∈ 𝑣 → (𝑧 ≠ ∅ → 𝜓)))
26	25	ralimi2 3100	. . . . 5 ⊢ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
27	26	eximi 1868	. . . 4 ⊢ (∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
28	22, 27	imim12i 63	. . 3 ⊢ (((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
29	11, 28	sylg 1856	. 2 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
30		raleq 3323	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑤 ∈ 𝑥 𝜑))
31	30	raleqbi1dv 3336	. . . 4 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑))
32		raleq 3323	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
33	32	exbidv 1954	. . . 4 ⊢ (𝑣 = 𝑥 → (∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
34	31, 33	imbi12d 347	. . 3 ⊢ (𝑣 = 𝑥 → ((∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))))
35	34	cbvalvw 2069	. 2 ⊢ (∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
36	29, 35	sylib 221	1 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2961  ∀wral 3082  {crab 3419  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-in 3915  df-ss 3925  df-pw 4569

This theorem is used by:  kmlem13  10165