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 e. V -> ( toInc ` ( ~P A i^i Fin ) ) e. Dirset )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
3 1 2 syl 
 |-  ( A e. V -> ( ~P A i^i Fin ) e. _V )
4 0elpw 
 |-  (/) e. ~P A
5 0fi 
 |-  (/) e. Fin
6 4 5 elini 
 |-  (/) e. ( ~P A i^i Fin )
7 ne0i 
 |-  ( (/) e. ( ~P A i^i Fin ) -> ( ~P A i^i Fin ) =/= (/) )
8 6 7 mp1i 
 |-  ( A e. V -> ( ~P A i^i Fin ) =/= (/) )
9 elin 
 |-  ( x e. ( ~P A i^i Fin ) <-> ( x e. ~P A /\ x e. Fin ) )
10 elin 
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y e. ~P A /\ y e. Fin ) )
11 pwuncl 
 |-  ( ( x e. ~P A /\ y e. ~P A ) -> ( x u. y ) e. ~P A )
12 11 ad2ant2r 
 |-  ( ( ( x e. ~P A /\ x e. Fin ) /\ ( y e. ~P A /\ y e. Fin ) ) -> ( x u. y ) e. ~P A )
13 unfi 
 |-  ( ( x e. Fin /\ y e. Fin ) -> ( x u. y ) e. Fin )
14 13 ad2ant2l 
 |-  ( ( ( x e. ~P A /\ x e. Fin ) /\ ( y e. ~P A /\ y e. Fin ) ) -> ( x u. y ) e. Fin )
15 12 14 elind 
 |-  ( ( ( x e. ~P A /\ x e. Fin ) /\ ( y e. ~P A /\ y e. Fin ) ) -> ( x u. y ) e. ( ~P A i^i Fin ) )
16 9 10 15 syl2anb 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y e. ( ~P A i^i Fin ) ) -> ( x u. y ) e. ( ~P A i^i Fin ) )
17 ssid 
 |-  ( x u. y ) C_ ( x u. y )
18 sseq2 
 |-  ( z = ( x u. y ) -> ( ( x u. y ) C_ z <-> ( x u. y ) C_ ( x u. y ) ) )
19 18 rspcev 
 |-  ( ( ( x u. y ) e. ( ~P A i^i Fin ) /\ ( x u. y ) C_ ( x u. y ) ) -> E. z e. ( ~P A i^i Fin ) ( x u. y ) C_ z )
20 16 17 19 sylancl 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ y e. ( ~P A i^i Fin ) ) -> E. z e. ( ~P A i^i Fin ) ( x u. y ) C_ z )
21 20 rgen2 
 |-  A. x e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) E. z e. ( ~P A i^i Fin ) ( x u. y ) C_ z
22 21 a1i 
 |-  ( A e. V -> A. x e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) E. z e. ( ~P A i^i Fin ) ( x u. y ) C_ z )
23 isipodrs 
 |-  ( ( toInc ` ( ~P A i^i Fin ) ) e. Dirset <-> ( ( ~P A i^i Fin ) e. _V /\ ( ~P A i^i Fin ) =/= (/) /\ A. x e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) E. z e. ( ~P A i^i Fin ) ( x u. y ) C_ z ) )
24 3 8 22 23 syl3anbrc 
 |-  ( A e. V -> ( toInc ` ( ~P A i^i Fin ) ) e. Dirset )