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 A Dirset A V A x A y A z A x y z

Proof

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