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 ( 𝐴 ∈ 𝑉 → ( toInc ‘ ( 𝒫 𝐴 ∩ Fin ) ) ∈ Dirset )

Proof

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