Theorem kmlem9

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

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

Proof

Step	Hyp	Ref	Expression
1		kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2		vex	⊢ 𝑧 ∈ V
3		eqeq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
4	3	rexbidv	⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
5	2 4 1	elab2	⊢ ( 𝑧 ∈ 𝐴 ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
6		vex	⊢ 𝑤 ∈ V
7		eqeq1	⊢ ( 𝑢 = 𝑤 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
8	7	rexbidv	⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
9	6 8 1	elab2	⊢ ( 𝑤 ∈ 𝐴 ↔ ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
10		difeq1	⊢ ( 𝑡 = ℎ → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
11		sneq	⊢ ( 𝑡 = ℎ → { 𝑡 } = { ℎ } )
12	11	difeq2d	⊢ ( 𝑡 = ℎ → ( 𝑥 ∖ { 𝑡 } ) = ( 𝑥 ∖ { ℎ } ) )
13	12	unieqd	⊢ ( 𝑡 = ℎ → ∪ ( 𝑥 ∖ { 𝑡 } ) = ∪ ( 𝑥 ∖ { ℎ } ) )
14	13	difeq2d	⊢ ( 𝑡 = ℎ → ( ℎ ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
15	10 14	eqtrd	⊢ ( 𝑡 = ℎ → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
16	15	eqeq2d	⊢ ( 𝑡 = ℎ → ( 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
17	16	cbvrexvw	⊢ ( ∃ 𝑡 ∈ 𝑥 𝑤 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
18	9 17	bitri	⊢ ( 𝑤 ∈ 𝐴 ↔ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) )
19		reeanv	⊢ ( ∃ 𝑡 ∈ 𝑥 ∃ ℎ ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
20		eqeq12	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 = 𝑤 ↔ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
21	15 20	imbitrrid	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑡 = ℎ → 𝑧 = 𝑤 ) )
22	21	necon3d	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → 𝑡 ≠ ℎ ) )
23		kmlem5	⊢ ( ( ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ ) → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) = ∅ )
24		ineq12	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ∩ 𝑤 ) = ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) )
25	24	eqeq1d	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) = ∅ ) )
26	23 25	imbitrrid	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ( ℎ ∈ 𝑥 ∧ 𝑡 ≠ ℎ ) → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
27	26	expd	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ℎ ∈ 𝑥 → ( 𝑡 ≠ ℎ → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
28	22 27	syl5d	⊢ ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( ℎ ∈ 𝑥 → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
29	28	com12	⊢ ( ℎ ∈ 𝑥 → ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
30	29	adantl	⊢ ( ( 𝑡 ∈ 𝑥 ∧ ℎ ∈ 𝑥 ) → ( ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
31	30	rexlimivv	⊢ ( ∃ 𝑡 ∈ 𝑥 ∃ ℎ ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
32	19 31	sylbir	⊢ ( ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∧ ∃ ℎ ∈ 𝑥 𝑤 = ( ℎ ∖ ∪ ( 𝑥 ∖ { ℎ } ) ) ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
33	5 18 32	syl2anb	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
34	33	rgen2	⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ )