Theorem kmlem1 9578

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 3499	. . . . . 6 ⊢ 𝑣 ∈ V
2	1	rabex 5237	. . . . 5 ⊢ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ∈ V
3		raleq 3407	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅))
4		raleq 3407	. . . . . . . 8 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
5	4	raleqbi1dv 3405	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
6	3, 5	anbi12d 632	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)))
7		raleq 3407	. . . . . . 7 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∀𝑧 ∈ 𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
8	7	exbidv 1922	. . . . . 6 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (∃𝑦∀𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
9	6, 8	imbi12d 347	. . . . 5 ⊢ (𝑥 = {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓)))
10	2, 9	spcv 3608	. . . 4 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
11	10	alrimiv 1928	. . 3 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓))
12		elrabi 3677	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ∈ 𝑣)
13		elrabi 3677	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑤 ∈ 𝑣)
14	13	imim1i 63	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑣 → 𝜑) → (𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜑))
15	14	ralimi2 3159	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑣 𝜑 → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
16	12, 15	imim12i 62	. . . . . 6 ⊢ ((𝑧 ∈ 𝑣 → ∀𝑤 ∈ 𝑣 𝜑) → (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
17	16	ralimi2 3159	. . . . 5 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑)
18		neeq1 3080	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
19	18	elrab 3682	. . . . . . 7 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} ↔ (𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅))
20	19	simprbi 499	. . . . . 6 ⊢ (𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝑧 ≠ ∅)
21	20	rgen 3150	. . . . 5 ⊢ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅
22	17, 21	jctil 522	. . . 4 ⊢ (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑))
23	19	biimpri 230	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅})
24	23	imim1i 63	. . . . . . 7 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → ((𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅) → 𝜓))
25	24	expd 418	. . . . . 6 ⊢ ((𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅} → 𝜓) → (𝑧 ∈ 𝑣 → (𝑧 ≠ ∅ → 𝜓)))
26	25	ralimi2 3159	. . . . 5 ⊢ (∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
27	26	eximi 1835	. . . 4 ⊢ (∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓))
28	22, 27	imim12i 62	. . 3 ⊢ (((∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}∀𝑤 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜑) → ∃𝑦∀𝑧 ∈ {𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅}𝜓) → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
29	11, 28	sylg 1823	. 2 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)))
30		raleq 3407	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑤 ∈ 𝑥 𝜑))
31	30	raleqbi1dv 3405	. . . 4 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑))
32		raleq 3407	. . . . 5 ⊢ (𝑣 = 𝑥 → (∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
33	32	exbidv 1922	. . . 4 ⊢ (𝑣 = 𝑥 → (∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
34	31, 33	imbi12d 347	. . 3 ⊢ (𝑣 = 𝑥 → ((∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))))
35	34	cbvalvw 2043	. 2 ⊢ (∀𝑣(∀𝑧 ∈ 𝑣 ∀𝑤 ∈ 𝑣 𝜑 → ∃𝑦∀𝑧 ∈ 𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
36	29, 35	sylib 220	1 ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140  {crab 3144  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954

This theorem is referenced by:  kmlem13  9590