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 0fin ⊢∅∈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∩Finx∪y⊆z
20 16 17 19 sylancl ⊢x∈𝒫A∩Fin∧y∈𝒫A∩Fin→∃z∈𝒫A∩Finx∪y⊆z
21 20 rgen2 ⊢∀x∈𝒫A∩Fin∀y∈𝒫A∩Fin∃z∈𝒫A∩Finx∪y⊆z
22 21 a1i ⊢A∈V→∀x∈𝒫A∩Fin∀y∈𝒫A∩Fin∃z∈𝒫A∩Finx∪y⊆z
23 isipodrs ⊢toInc⁡𝒫A∩Fin∈Dirset↔𝒫A∩Fin∈V∧𝒫A∩Fin≠∅∧∀x∈𝒫A∩Fin∀y∈𝒫A∩Fin∃z∈𝒫A∩Finx∪y⊆z
24 3 8 22 23 syl3anbrc ⊢A∈V→toInc⁡𝒫A∩Fin∈Dirset