Metamath Proof Explorer

Theorem isipodrs

Description: Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isipodrs ( ( toInc ‘ 𝐴 ) ∈ Dirset ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ ( toInc ‘ 𝐴 ) ) = ( Base ‘ ( toInc ‘ 𝐴 ) )
2 1 drsbn0 ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ )
3 2 neneqd ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → ¬ ( Base ‘ ( toInc ‘ 𝐴 ) ) = ∅ )
4 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( toInc ‘ 𝐴 ) = ∅ )
5 4 fveq2d ⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ ( toInc ‘ 𝐴 ) ) = ( Base ‘ ∅ ) )
6 base0 ⊢ ∅ = ( Base ‘ ∅ )
7 5 6 eqtr4di ⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ ( toInc ‘ 𝐴 ) ) = ∅ )
8 3 7 nsyl2 ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → 𝐴 ∈ V )
9 simp1 ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) → 𝐴 ∈ V )
10 eqid ⊢ ( le ‘ ( toInc ‘ 𝐴 ) ) = ( le ‘ ( toInc ‘ 𝐴 ) )
11 1 10 isdrs ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset ↔ ( ( toInc ‘ 𝐴 ) ∈ Proset ∧ ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) )
12 eqid ⊢ ( toInc ‘ 𝐴 ) = ( toInc ‘ 𝐴 )
13 12 ipopos ⊢ ( toInc ‘ 𝐴 ) ∈ Poset
14 posprs ⊢ ( ( toInc ‘ 𝐴 ) ∈ Poset → ( toInc ‘ 𝐴 ) ∈ Proset )
15 13 14 mp1i ⊢ ( 𝐴 ∈ V → ( toInc ‘ 𝐴 ) ∈ Proset )
16 id ⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
17 15 16 2thd ⊢ ( 𝐴 ∈ V → ( ( toInc ‘ 𝐴 ) ∈ Proset ↔ 𝐴 ∈ V ) )
18 12 ipobas ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) )
19 neeq1 ⊢ ( 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) → ( 𝐴 ≠ ∅ ↔ ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ) )
20 rexeq ⊢ ( 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) )
21 20 raleqbi1dv ⊢ ( 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) )
22 21 raleqbi1dv ⊢ ( 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) )
23 19 22 anbi12d ⊢ ( 𝐴 = ( Base ‘ ( toInc ‘ 𝐴 ) ) → ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ) )
24 18 23 syl ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ) )
25 simpll ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ∈ V )
26 simplrl ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
27 simpr ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
28 12 10 ipole ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑥 ⊆ 𝑧 ) )
29 25 26 27 28 syl3anc ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑥 ⊆ 𝑧 ) )
30 simplrr ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
31 12 10 ipole ⊢ ( ( 𝐴 ∈ V ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑦 ⊆ 𝑧 ) )
32 25 30 27 31 syl3anc ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ↔ 𝑦 ⊆ 𝑧 ) )
33 29 32 anbi12d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑧 ) ) )
34 unss ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑧 ) ↔ ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 )
35 33 34 bitrdi ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )
36 35 rexbidva ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )
37 36 2ralbidva ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )
38 37 anbi2d ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) )
39 24 38 bitr3d ⊢ ( 𝐴 ∈ V → ( ( ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) )
40 17 39 anbi12d ⊢ ( 𝐴 ∈ V → ( ( ( toInc ‘ 𝐴 ) ∈ Proset ∧ ( ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ) ↔ ( 𝐴 ∈ V ∧ ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) ) )
41 3anass ⊢ ( ( ( toInc ‘ 𝐴 ) ∈ Proset ∧ ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( ( toInc ‘ 𝐴 ) ∈ Proset ∧ ( ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ) )
42 3anass ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝐴 ∈ V ∧ ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) )
43 40 41 42 3bitr4g ⊢ ( 𝐴 ∈ V → ( ( ( toInc ‘ 𝐴 ) ∈ Proset ∧ ( Base ‘ ( toInc ‘ 𝐴 ) ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ∃ 𝑧 ∈ ( Base ‘ ( toInc ‘ 𝐴 ) ) ( 𝑥 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ∧ 𝑦 ( le ‘ ( toInc ‘ 𝐴 ) ) 𝑧 ) ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) )
44 11 43 syl5bb ⊢ ( 𝐴 ∈ V → ( ( toInc ‘ 𝐴 ) ∈ Dirset ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) ) )
45 8 9 44 pm5.21nii ⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )