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 ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ∃ 𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧 )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → 𝑋 ⊆ 𝐴 )
2 ipodrscl ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → 𝐴 ∈ V )
3 eqid ⊢ ( toInc ‘ 𝐴 ) = ( toInc ‘ 𝐴 )
4 3 ipobas ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) )
5 2 4 syl ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) )
6 5 3ad2ant1 ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) )
7 1 6 sseqtrd ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → 𝑋 ⊆ ( Base ‘ ( toInc ‘ 𝐴 ) ) )
8 eqid ⊢ ( Base ‘ ( toInc ‘ 𝐴 ) ) = ( Base ‘ ( toInc ‘ 𝐴 ) )
9 eqid ⊢ ( le ‘ ( toInc ‘ 𝐴 ) ) = ( le ‘ ( toInc ‘ 𝐴 ) )
10 8 9 drsdirfi ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∧ 𝑋 ∈ Fin ) → ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 )
11 7 10 syld3an2 ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 )
12 6 rexeqdv ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ( ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) )
13 2 3ad2ant1 ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → 𝐴 ∈ V )
14 13 adantr ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐴 ∈ V )
15 1 sselda ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝐴 )
16 15 adantrl ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑤 ∈ 𝐴 )
17 simprl ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝐴 )
18 3 9 ipole ⊢ ( ( 𝐴 ∈ V ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑤 ⊆ 𝑧 ) )
19 14 16 17 18 syl3anc ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑤 ⊆ 𝑧 ) )
20 19 anassrs ⊢ ( ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑤 ⊆ 𝑧 ) )
21 20 ralbidva ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ 𝑧 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ ∀ 𝑤 ∈ 𝑋 𝑤 ⊆ 𝑧 ) )
22 unissb ⊢ ( ∪ 𝑋 ⊆ 𝑧 ↔ ∀ 𝑤 ∈ 𝑋 𝑤 ⊆ 𝑧 )
23 21 22 bitr4di ⊢ ( ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) ∧ 𝑧 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ ∪ 𝑋 ⊆ 𝑧 ) )
24 23 rexbidva ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ( ∃ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧 ) )
25 12 24 bitr3d ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ( ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑤 ∈ 𝑋 𝑤 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧 ) )
26 11 25 mpbid ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) → ∃ 𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧 )