Metamath Proof Explorer

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 syl5req ⊢ ( 𝑧 ∈ 𝑥 → 𝑥 = ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
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 syl5eq ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧 ) → ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ∅ )
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 syl5eq ⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ ( { 𝑧 } ∪ ( 𝑥 ∖ { 𝑧 } ) ) ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) )
41 15 40 eqtrd ⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) )
42 un0 ⊢ ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) = ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
43 indif ⊢ ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) )
44 42 43 eqtri ⊢ ( ( 𝑧 ∩ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ) ∪ ∅ ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) )
45 41 44 eqtrdi ⊢ ( 𝑧 ∈ 𝑥 → ∪ 𝑡 ∈ 𝑥 ( 𝑧 ∩ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
46 9 45 syl5eq ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )