Metamath Proof Explorer

Theorem fpwipodrs

Description: The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion fpwipodrs ⊢ A ∈ V → toInc ⁡ 𝒫 A ∩ Fin ∈ Dirset

Proof

Step Hyp Ref Expression
1 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
2 inex1g ⊢ 𝒫 A ∈ V → 𝒫 A ∩ Fin ∈ V
3 1 2 syl ⊢ A ∈ V → 𝒫 A ∩ Fin ∈ V
4 0elpw ⊢ ∅ ∈ 𝒫 A
5 0fi ⊢ ∅ ∈ Fin
6 4 5 elini ⊢ ∅ ∈ 𝒫 A ∩ Fin
7 ne0i ⊢ ∅ ∈ 𝒫 A ∩ Fin → 𝒫 A ∩ Fin ≠ ∅
8 6 7 mp1i ⊢ A ∈ V → 𝒫 A ∩ Fin ≠ ∅
9 elin ⊢ x ∈ 𝒫 A ∩ Fin ↔ x ∈ 𝒫 A ∧ x ∈ Fin
10 elin ⊢ y ∈ 𝒫 A ∩ Fin ↔ y ∈ 𝒫 A ∧ y ∈ Fin
11 pwuncl ⊢ x ∈ 𝒫 A ∧ y ∈ 𝒫 A → x ∪ y ∈ 𝒫 A
12 11 ad2ant2r ⊢ x ∈ 𝒫 A ∧ x ∈ Fin ∧ y ∈ 𝒫 A ∧ y ∈ Fin → x ∪ y ∈ 𝒫 A
13 unfi ⊢ x ∈ Fin ∧ y ∈ Fin → x ∪ y ∈ Fin
14 13 ad2ant2l ⊢ x ∈ 𝒫 A ∧ x ∈ Fin ∧ y ∈ 𝒫 A ∧ y ∈ Fin → x ∪ y ∈ Fin
15 12 14 elind ⊢ x ∈ 𝒫 A ∧ x ∈ Fin ∧ y ∈ 𝒫 A ∧ y ∈ Fin → x ∪ y ∈ 𝒫 A ∩ Fin
16 9 10 15 syl2anb ⊢ x ∈ 𝒫 A ∩ Fin ∧ y ∈ 𝒫 A ∩ Fin → x ∪ y ∈ 𝒫 A ∩ Fin
17 ssid ⊢ x ∪ y ⊆ x ∪ y
18 sseq2 ⊢ z = x ∪ y → x ∪ y ⊆ z ↔ x ∪ y ⊆ x ∪ y
19 18 rspcev ⊢ x ∪ y ∈ 𝒫 A ∩ Fin ∧ x ∪ y ⊆ x ∪ y → ∃ z ∈ 𝒫 A ∩ Fin x ∪ y ⊆ z
20 16 17 19 sylancl ⊢ x ∈ 𝒫 A ∩ Fin ∧ y ∈ 𝒫 A ∩ Fin → ∃ z ∈ 𝒫 A ∩ Fin x ∪ y ⊆ z
21 20 rgen2 ⊢ ∀ x ∈ 𝒫 A ∩ Fin ∀ y ∈ 𝒫 A ∩ Fin ∃ z ∈ 𝒫 A ∩ Fin x ∪ y ⊆ z
22 21 a1i ⊢ A ∈ V → ∀ x ∈ 𝒫 A ∩ Fin ∀ y ∈ 𝒫 A ∩ Fin ∃ z ∈ 𝒫 A ∩ Fin x ∪ y ⊆ z
23 isipodrs ⊢ toInc ⁡ 𝒫 A ∩ Fin ∈ Dirset ↔ 𝒫 A ∩ Fin ∈ V ∧ 𝒫 A ∩ Fin ≠ ∅ ∧ ∀ x ∈ 𝒫 A ∩ Fin ∀ y ∈ 𝒫 A ∩ Fin ∃ z ∈ 𝒫 A ∩ Fin x ∪ y ⊆ z
24 3 8 22 23 syl3anbrc ⊢ A ∈ V → toInc ⁡ 𝒫 A ∩ Fin ∈ Dirset