Theorem kmlem11

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

	Ref	Expression
Hypothesis	kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion	kmlem11	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2	1	unieqi	⊢ ∪ 𝐴 = ∪ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
3		vex	⊢ 𝑡 ∈ V
4	3	difexi	⊢ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∈ V
5	4	dfiun2	⊢ ∪ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ∪ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
6	2 5	eqtr4i	⊢ ∪ 𝐴 = ∪ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) )
7	6	ineq2i	⊢ ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∩ ∪ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
8		iunin2	⊢ ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( 𝑧 ∩ ∪ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
9	7 8	eqtr4i	⊢ ( 𝑧 ∩ ∪ 𝐴 ) = ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
10		undif2	⊢ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) = ( { 𝑧 } ∪ 𝑥 )
11		snssi	⊢ ( 𝑧 ∈ 𝑥 → { 𝑧 } ⊆ 𝑥 )
12		ssequn1	⊢ ( { 𝑧 } ⊆ 𝑥 ↔ ( { 𝑧 } ∪ 𝑥 ) = 𝑥 )
13	11 12	sylib	⊢ ( 𝑧 ∈ 𝑥 → ( { 𝑧 } ∪ 𝑥 ) = 𝑥 )
14	10 13	eqtr2id	⊢ ( 𝑧 ∈ 𝑥 → 𝑥 = ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
15	14	iuneq1d	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∪ 𝑡 ∈ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
16		iunxun	⊢ ∪ 𝑡 ∈ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ∪ 𝑡 ∈ { 𝑧 } ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) ∪ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
17		vex	⊢ 𝑧 ∈ V
18		difeq1	⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
19		sneq	⊢ ( 𝑡 = 𝑧 → { 𝑡 } = { 𝑧 } )
20	19	difeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑥 ∖ { 𝑡 } ) = ( 𝑥 ∖ { 𝑧 } ) )
21	20	unieqd	⊢ ( 𝑡 = 𝑧 → ∪ ( 𝑥 ∖ { 𝑡 } ) = ∪ ( 𝑥 ∖ { 𝑧 } ) )
22	21	difeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
23	18 22	eqtrd	⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
24	23	ineq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) )
25	17 24	iunxsn	⊢ ∪ 𝑡 ∈ { 𝑧 } ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
26	25	uneq1i	⊢ ( ∪ 𝑡 ∈ { 𝑧 } ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) ∪ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
27	16 26	eqtri	⊢ ∪ 𝑡 ∈ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
28		eldifsni	⊢ ( 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) → 𝑡 ≠ 𝑧 )
29		incom	⊢ ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑧 )
30		kmlem4	⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧 ) → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑧 ) = ∅ )
31	29 30	eqtrid	⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧 ) → ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ )
32	31	ex	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑡 ≠ 𝑧 → ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ ) )
33	28 32	syl5	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) → ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ ) )
34	33	ralrimiv	⊢ ( 𝑧 ∈ 𝑥 → ∀ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ )
35		iuneq2	⊢ ( ∀ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ → ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ∅ )
36	34 35	syl	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ∅ )
37		iun0	⊢ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ∅ = ∅
38	36 37	eqtrdi	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ )
39	38	uneq2d	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∪ 𝑡 ∈ ( 𝑥 ∖ { 𝑧 } ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) )
40	27 39	eqtrid	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) )
41	15 40	eqtrd	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) )
42		un0	⊢ ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) = ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
43		indif	⊢ ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) )
44	42 43	eqtri	⊢ ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) )
45	41 44	eqtrdi	⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
46	9 45	eqtrid	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )