Metamath Proof Explorer

Theorem ipodrsfi

Description: Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion ipodrsfi ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈A⋃X⊆z

Proof

Step Hyp Ref Expression
1 simp2 ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→X⊆A
2 ipodrscl ⊢toInc⁡A∈Dirset→A∈V
3 eqid ⊢toInc⁡A=toInc⁡A
4 3 ipobas ⊢A∈V→A=BasetoInc⁡A
5 2 4 syl ⊢toInc⁡A∈Dirset→A=BasetoInc⁡A
6 5 3ad2ant1 ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→A=BasetoInc⁡A
7 1 6 sseqtrd ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→X⊆BasetoInc⁡A
8 eqid ⊢BasetoInc⁡A=BasetoInc⁡A
9 eqid ⊢≤toInc⁡A=≤toInc⁡A
10 8 9 drsdirfi ⊢toInc⁡A∈Dirset∧X⊆BasetoInc⁡A∧X∈Fin→∃z∈BasetoInc⁡A∀w∈Xw≤toInc⁡Az
11 7 10 syld3an2 ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈BasetoInc⁡A∀w∈Xw≤toInc⁡Az
12 6 rexeqdv ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈A∀w∈Xw≤toInc⁡Az↔∃z∈BasetoInc⁡A∀w∈Xw≤toInc⁡Az
13 2 3ad2ant1 ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→A∈V
14 13 adantr ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A∧w∈X→A∈V
15 1 sselda ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧w∈X→w∈A
16 15 adantrl ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A∧w∈X→w∈A
17 simprl ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A∧w∈X→z∈A
18 3 9 ipole ⊢A∈V∧w∈A∧z∈A→w≤toInc⁡Az↔w⊆z
19 14 16 17 18 syl3anc ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A∧w∈X→w≤toInc⁡Az↔w⊆z
20 19 anassrs ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A∧w∈X→w≤toInc⁡Az↔w⊆z
21 20 ralbidva ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A→∀w∈Xw≤toInc⁡Az↔∀w∈Xw⊆z
22 unissb ⊢⋃X⊆z↔∀w∈Xw⊆z
23 21 22 bitr4di ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin∧z∈A→∀w∈Xw≤toInc⁡Az↔⋃X⊆z
24 23 rexbidva ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈A∀w∈Xw≤toInc⁡Az↔∃z∈A⋃X⊆z
25 12 24 bitr3d ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈BasetoInc⁡A∀w∈Xw≤toInc⁡Az↔∃z∈A⋃X⊆z
26 11 25 mpbid ⊢toInc⁡A∈Dirset∧X⊆A∧X∈Fin→∃z∈A⋃X⊆z