Theorem kmlem12

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004)

	Ref	Expression
Hypothesis	kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion	kmlem12	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2		difeq1	⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
3		sneq	⊢ ( 𝑡 = 𝑧 → { 𝑡 } = { 𝑧 } )
4	3	difeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑥 ∖ { 𝑡 } ) = ( 𝑥 ∖ { 𝑧 } ) )
5	4	unieqd	⊢ ( 𝑡 = 𝑧 → ∪ ( 𝑥 ∖ { 𝑡 } ) = ∪ ( 𝑥 ∖ { 𝑧 } ) )
6	5	difeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
7	2 6	eqtrd	⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
8	7	neeq1d	⊢ ( 𝑡 = 𝑧 → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ↔ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ) )
9	8	cbvralvw	⊢ ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ )
10	7	ineq1d	⊢ ( 𝑡 = 𝑧 → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) = ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
11	10	eleq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
12	11	eubidv	⊢ ( 𝑡 = 𝑧 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
13	12	cbvralvw	⊢ ( ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
14	9 13	imbi12i	⊢ ( ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
15		in12	⊢ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) = ( 𝑦 ∩ ( 𝑧 ∩ ∪ 𝐴 ) )
16		incom	⊢ ( 𝑦 ∩ ( 𝑧 ∩ ∪ 𝐴 ) ) = ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 )
17	15 16	eqtri	⊢ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) = ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 )
18	1	kmlem11	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
19	18	ineq1d	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 ) = ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
20	17 19	syl5req	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) )
21	20	eleq2d	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
22	21	eubidv	⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
23		ax-1	⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
24	22 23	syl6bi	⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
25	24	ralimia	⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
26	25	imim2i	⊢ ( ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
27	14 26	sylbi	⊢ ( ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
28	1	raleqi	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
29		df-ral	⊢ ( ∀ 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
30		vex	⊢ 𝑧 ∈ V
31		eqeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
32	31	rexbidv	⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
33	30 32	elab	⊢ ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
34	33	imbi1i	⊢ ( ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
35		r19.23v	⊢ ( ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
36	34 35	bitr4i	⊢ ( ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
37	36	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑧 ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
38		ralcom4	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑧 ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
39		vex	⊢ 𝑡 ∈ V
40	39	difexi	⊢ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∈ V
41		neeq1	⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ ↔ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ) )
42		ineq1	⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ∩ 𝑦 ) = ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) )
43	42	eleq2d	⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
44	43	eubidv	⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
45	41 44	imbi12d	⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) ) )
46	40 45	ceqsalv	⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
47	46	ralbii	⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
48	37 38 47	3bitr2i	⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
49	28 29 48	3bitri	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
50		ralim	⊢ ( ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
51	49 50	sylbi	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
52	27 51	syl11	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )