Metamath Proof Explorer

Theorem ipodrsima

Description: The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypotheses ipodrsima.f ⊢φ→FFn𝒫A
ipodrsima.m ⊢φ∧u⊆v∧v⊆A→F⁡u⊆F⁡v
ipodrsima.d ⊢φ→toInc⁡B∈Dirset
ipodrsima.s ⊢φ→B⊆𝒫A
ipodrsima.a ⊢φ→FB∈V
Assertion ipodrsima ⊢φ→toInc⁡FB∈Dirset

Proof

Step Hyp Ref Expression
1 ipodrsima.f ⊢φ→FFn𝒫A
2 ipodrsima.m ⊢φ∧u⊆v∧v⊆A→F⁡u⊆F⁡v
3 ipodrsima.d ⊢φ→toInc⁡B∈Dirset
4 ipodrsima.s ⊢φ→B⊆𝒫A
5 ipodrsima.a ⊢φ→FB∈V
6 5 elexd ⊢φ→FB∈V
7 isipodrs ⊢toInc⁡B∈Dirset↔B∈V∧B≠∅∧∀a∈B∀b∈B∃c∈Ba∪b⊆c
8 3 7 sylib ⊢φ→B∈V∧B≠∅∧∀a∈B∀b∈B∃c∈Ba∪b⊆c
9 8 simp2d ⊢φ→B≠∅
10 fnimaeq0 ⊢FFn𝒫A∧B⊆𝒫A→FB=∅↔B=∅
11 1 4 10 syl2anc ⊢φ→FB=∅↔B=∅
12 11 necon3bid ⊢φ→FB≠∅↔B≠∅
13 9 12 mpbird ⊢φ→FB≠∅
14 8 simp3d ⊢φ→∀a∈B∀b∈B∃c∈Ba∪b⊆c
15 simplll ⊢φ∧a∈B∧b∈B∧c∈B∧a⊆c→φ
16 simpr ⊢φ∧a∈B∧b∈B∧c∈B∧a⊆c→a⊆c
17 4 ad2antrr ⊢φ∧a∈B∧b∈B∧c∈B→B⊆𝒫A
18 simprr ⊢φ∧a∈B∧b∈B∧c∈B→c∈B
19 17 18 sseldd ⊢φ∧a∈B∧b∈B∧c∈B→c∈𝒫A
20 19 elpwid ⊢φ∧a∈B∧b∈B∧c∈B→c⊆A
21 20 adantr ⊢φ∧a∈B∧b∈B∧c∈B∧a⊆c→c⊆A
22 vex ⊢a∈V
23 vex ⊢c∈V
24 sseq12 ⊢u=a∧v=c→u⊆v↔a⊆c
25 sseq1 ⊢v=c→v⊆A↔c⊆A
26 25 adantl ⊢u=a∧v=c→v⊆A↔c⊆A
27 24 26 anbi12d ⊢u=a∧v=c→u⊆v∧v⊆A↔a⊆c∧c⊆A
28 27 anbi2d ⊢u=a∧v=c→φ∧u⊆v∧v⊆A↔φ∧a⊆c∧c⊆A
29 fveq2 ⊢u=a→F⁡u=F⁡a
30 fveq2 ⊢v=c→F⁡v=F⁡c
31 sseq12 ⊢F⁡u=F⁡a∧F⁡v=F⁡c→F⁡u⊆F⁡v↔F⁡a⊆F⁡c
32 29 30 31 syl2an ⊢u=a∧v=c→F⁡u⊆F⁡v↔F⁡a⊆F⁡c
33 28 32 imbi12d ⊢u=a∧v=c→φ∧u⊆v∧v⊆A→F⁡u⊆F⁡v↔φ∧a⊆c∧c⊆A→F⁡a⊆F⁡c
34 22 23 33 2 vtocl2 ⊢φ∧a⊆c∧c⊆A→F⁡a⊆F⁡c
35 15 16 21 34 syl12anc ⊢φ∧a∈B∧b∈B∧c∈B∧a⊆c→F⁡a⊆F⁡c
36 35 ex ⊢φ∧a∈B∧b∈B∧c∈B→a⊆c→F⁡a⊆F⁡c
37 simplll ⊢φ∧a∈B∧b∈B∧c∈B∧b⊆c→φ
38 simpr ⊢φ∧a∈B∧b∈B∧c∈B∧b⊆c→b⊆c
39 20 adantr ⊢φ∧a∈B∧b∈B∧c∈B∧b⊆c→c⊆A
40 vex ⊢b∈V
41 sseq12 ⊢u=b∧v=c→u⊆v↔b⊆c
42 25 adantl ⊢u=b∧v=c→v⊆A↔c⊆A
43 41 42 anbi12d ⊢u=b∧v=c→u⊆v∧v⊆A↔b⊆c∧c⊆A
44 43 anbi2d ⊢u=b∧v=c→φ∧u⊆v∧v⊆A↔φ∧b⊆c∧c⊆A
45 fveq2 ⊢u=b→F⁡u=F⁡b
46 sseq12 ⊢F⁡u=F⁡b∧F⁡v=F⁡c→F⁡u⊆F⁡v↔F⁡b⊆F⁡c
47 45 30 46 syl2an ⊢u=b∧v=c→F⁡u⊆F⁡v↔F⁡b⊆F⁡c
48 44 47 imbi12d ⊢u=b∧v=c→φ∧u⊆v∧v⊆A→F⁡u⊆F⁡v↔φ∧b⊆c∧c⊆A→F⁡b⊆F⁡c
49 40 23 48 2 vtocl2 ⊢φ∧b⊆c∧c⊆A→F⁡b⊆F⁡c
50 37 38 39 49 syl12anc ⊢φ∧a∈B∧b∈B∧c∈B∧b⊆c→F⁡b⊆F⁡c
51 50 ex ⊢φ∧a∈B∧b∈B∧c∈B→b⊆c→F⁡b⊆F⁡c
52 36 51 anim12d ⊢φ∧a∈B∧b∈B∧c∈B→a⊆c∧b⊆c→F⁡a⊆F⁡c∧F⁡b⊆F⁡c
53 unss ⊢a⊆c∧b⊆c↔a∪b⊆c
54 unss ⊢F⁡a⊆F⁡c∧F⁡b⊆F⁡c↔F⁡a∪F⁡b⊆F⁡c
55 52 53 54 3imtr3g ⊢φ∧a∈B∧b∈B∧c∈B→a∪b⊆c→F⁡a∪F⁡b⊆F⁡c
56 55 anassrs ⊢φ∧a∈B∧b∈B∧c∈B→a∪b⊆c→F⁡a∪F⁡b⊆F⁡c
57 56 reximdva ⊢φ∧a∈B∧b∈B→∃c∈Ba∪b⊆c→∃c∈BF⁡a∪F⁡b⊆F⁡c
58 57 ralimdva ⊢φ∧a∈B→∀b∈B∃c∈Ba∪b⊆c→∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
59 58 ralimdva ⊢φ→∀a∈B∀b∈B∃c∈Ba∪b⊆c→∀a∈B∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
60 14 59 mpd ⊢φ→∀a∈B∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
61 uneq1 ⊢x=F⁡a→x∪y=F⁡a∪y
62 61 sseq1d ⊢x=F⁡a→x∪y⊆z↔F⁡a∪y⊆z
63 62 rexbidv ⊢x=F⁡a→∃z∈FBx∪y⊆z↔∃z∈FBF⁡a∪y⊆z
64 63 ralbidv ⊢x=F⁡a→∀y∈FB∃z∈FBx∪y⊆z↔∀y∈FB∃z∈FBF⁡a∪y⊆z
65 64 ralima ⊢FFn𝒫A∧B⊆𝒫A→∀x∈FB∀y∈FB∃z∈FBx∪y⊆z↔∀a∈B∀y∈FB∃z∈FBF⁡a∪y⊆z
66 1 4 65 syl2anc ⊢φ→∀x∈FB∀y∈FB∃z∈FBx∪y⊆z↔∀a∈B∀y∈FB∃z∈FBF⁡a∪y⊆z
67 uneq2 ⊢y=F⁡b→F⁡a∪y=F⁡a∪F⁡b
68 67 sseq1d ⊢y=F⁡b→F⁡a∪y⊆z↔F⁡a∪F⁡b⊆z
69 68 rexbidv ⊢y=F⁡b→∃z∈FBF⁡a∪y⊆z↔∃z∈FBF⁡a∪F⁡b⊆z
70 69 ralima ⊢FFn𝒫A∧B⊆𝒫A→∀y∈FB∃z∈FBF⁡a∪y⊆z↔∀b∈B∃z∈FBF⁡a∪F⁡b⊆z
71 1 4 70 syl2anc ⊢φ→∀y∈FB∃z∈FBF⁡a∪y⊆z↔∀b∈B∃z∈FBF⁡a∪F⁡b⊆z
72 sseq2 ⊢z=F⁡c→F⁡a∪F⁡b⊆z↔F⁡a∪F⁡b⊆F⁡c
73 72 rexima ⊢FFn𝒫A∧B⊆𝒫A→∃z∈FBF⁡a∪F⁡b⊆z↔∃c∈BF⁡a∪F⁡b⊆F⁡c
74 1 4 73 syl2anc ⊢φ→∃z∈FBF⁡a∪F⁡b⊆z↔∃c∈BF⁡a∪F⁡b⊆F⁡c
75 74 ralbidv ⊢φ→∀b∈B∃z∈FBF⁡a∪F⁡b⊆z↔∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
76 71 75 bitrd ⊢φ→∀y∈FB∃z∈FBF⁡a∪y⊆z↔∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
77 76 ralbidv ⊢φ→∀a∈B∀y∈FB∃z∈FBF⁡a∪y⊆z↔∀a∈B∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
78 66 77 bitrd ⊢φ→∀x∈FB∀y∈FB∃z∈FBx∪y⊆z↔∀a∈B∀b∈B∃c∈BF⁡a∪F⁡b⊆F⁡c
79 60 78 mpbird ⊢φ→∀x∈FB∀y∈FB∃z∈FBx∪y⊆z
80 isipodrs ⊢toInc⁡FB∈Dirset↔FB∈V∧FB≠∅∧∀x∈FB∀y∈FB∃z∈FBx∪y⊆z
81 6 13 79 80 syl3anbrc ⊢φ→toInc⁡FB∈Dirset