Metamath Proof Explorer

Theorem infssuni

Description: If an infinite set A is included in the underlying set of a finite cover B , then there exists a set of the cover that contains an infinite number of element of A . (Contributed by FL, 2-Aug-2009)

Ref Expression
Assertion infssuni ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 dfral2 ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin ↔ ¬ ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin )
2 iunfi ⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin ) → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin )
3 iunin2 ⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) = ( 𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥 )
4 3 eleq1i ⊢ ( ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥 ) ∈ Fin )
5 uniiun ⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
6 5 eqcomi ⊢ ∪ 𝑥 ∈ 𝐵 𝑥 = ∪ 𝐵
7 6 ineq2i ⊢ ( 𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥 ) = ( 𝐴 ∩ ∪ 𝐵 )
8 7 eleq1i ⊢ ( ( 𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥 ) ∈ Fin ↔ ( 𝐴 ∩ ∪ 𝐵 ) ∈ Fin )
9 dfss2 ⊢ ( 𝐴 ⊆ ∪ 𝐵 ↔ ( 𝐴 ∩ ∪ 𝐵 ) = 𝐴 )
10 eleq1 ⊢ ( ( 𝐴 ∩ ∪ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ ∪ 𝐵 ) ∈ Fin ↔ 𝐴 ∈ Fin ) )
11 pm2.24 ⊢ ( 𝐴 ∈ Fin → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) )
12 10 11 biimtrdi ⊢ ( ( 𝐴 ∩ ∪ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ ∪ 𝐵 ) ∈ Fin → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
13 9 12 sylbi ⊢ ( 𝐴 ⊆ ∪ 𝐵 → ( ( 𝐴 ∩ ∪ 𝐵 ) ∈ Fin → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
14 13 com12 ⊢ ( ( 𝐴 ∩ ∪ 𝐵 ) ∈ Fin → ( 𝐴 ⊆ ∪ 𝐵 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
15 8 14 sylbi ⊢ ( ( 𝐴 ∩ ∪ 𝑥 ∈ 𝐵 𝑥 ) ∈ Fin → ( 𝐴 ⊆ ∪ 𝐵 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
16 4 15 sylbi ⊢ ( ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin → ( 𝐴 ⊆ ∪ 𝐵 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
17 2 16 syl ⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin ) → ( 𝐴 ⊆ ∪ 𝐵 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) )
18 17 ex ⊢ ( 𝐵 ∈ Fin → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin → ( 𝐴 ⊆ ∪ 𝐵 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) ) )
19 18 com24 ⊢ ( 𝐵 ∈ Fin → ( ¬ 𝐴 ∈ Fin → ( 𝐴 ⊆ ∪ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) ) ) )
20 19 3imp21 ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ∩ 𝑥 ) ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) )
21 1 20 biimtrrid ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵 ) → ( ¬ ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin ) )
22 21 pm2.18d ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ¬ ( 𝐴 ∩ 𝑥 ) ∈ Fin )