Theorem kmlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑣 ∈ V
2	1	rabex	⊢ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∈ V
3		raleq	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ) )
4		raleq	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ∀ 𝑤 ∈ 𝑥 𝜑 ↔ ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) )
5	4	raleqbi1dv	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ↔ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) )
6	3 5	anbi12d	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) ↔ ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) ) )
7		raleq	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ∀ 𝑧 ∈ 𝑥 𝜓 ↔ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) )
8	7	exbidv	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ↔ ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) )
9	6 8	imbi12d	⊢ ( 𝑥 = { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ) ↔ ( ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) ) )
10	2 9	spcv	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ) → ( ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) )
11	10	alrimiv	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ) → ∀ 𝑣 ( ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) )
12		elrabi	⊢ ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝑧 ∈ 𝑣 )
13		elrabi	⊢ ( 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝑤 ∈ 𝑣 )
14	13	imim1i	⊢ ( ( 𝑤 ∈ 𝑣 → 𝜑 ) → ( 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝜑 ) )
15	14	ralimi2	⊢ ( ∀ 𝑤 ∈ 𝑣 𝜑 → ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 )
16	12 15	imim12i	⊢ ( ( 𝑧 ∈ 𝑣 → ∀ 𝑤 ∈ 𝑣 𝜑 ) → ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) )
17	16	ralimi2	⊢ ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 )
18		neeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
19	18	elrab	⊢ ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅ ) )
20	19	simprbi	⊢ ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝑧 ≠ ∅ )
21	20	rgen	⊢ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅
22	17 21	jctil	⊢ ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) )
23	19	biimpri	⊢ ( ( 𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅ ) → 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } )
24	23	imim1i	⊢ ( ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝜓 ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑧 ≠ ∅ ) → 𝜓 ) )
25	24	expd	⊢ ( ( 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } → 𝜓 ) → ( 𝑧 ∈ 𝑣 → ( 𝑧 ≠ ∅ → 𝜓 ) ) )
26	25	ralimi2	⊢ ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 → ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) )
27	26	eximi	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) )
28	22 27	imim12i	⊢ ( ( ( ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } ∀ 𝑤 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ { 𝑢 ∈ 𝑣 ∣ 𝑢 ≠ ∅ } 𝜓 ) → ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ) )
29	11 28	sylg	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ) → ∀ 𝑣 ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ) )
30		raleq	⊢ ( 𝑣 = 𝑥 → ( ∀ 𝑤 ∈ 𝑣 𝜑 ↔ ∀ 𝑤 ∈ 𝑥 𝜑 ) )
31	30	raleqbi1dv	⊢ ( 𝑣 = 𝑥 → ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) )
32		raleq	⊢ ( 𝑣 = 𝑥 → ( ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → 𝜓 ) ) )
33	32	exbidv	⊢ ( 𝑣 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → 𝜓 ) ) )
34	31 33	imbi12d	⊢ ( 𝑣 = 𝑥 → ( ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ) ↔ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → 𝜓 ) ) ) )
35	34	cbvalvw	⊢ ( ∀ 𝑣 ( ∀ 𝑧 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑣 ( 𝑧 ≠ ∅ → 𝜓 ) ) ↔ ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → 𝜓 ) ) )
36	29 35	sylib	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 𝜓 ) → ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → 𝜓 ) ) )