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 ⊢ φ → F Fn 𝒫 A
ipodrsima.m ⊢ φ ∧ u ⊆ v ∧ v ⊆ A → F ⁡ u ⊆ F ⁡ v
ipodrsima.d ⊢ φ → toInc ⁡ B ∈ Dirset
ipodrsima.s ⊢ φ → B ⊆ 𝒫 A
ipodrsima.a ⊢ φ → F B ∈ V
Assertion ipodrsima ⊢ φ → toInc ⁡ F B ∈ Dirset

Proof

Step Hyp Ref Expression
1 ipodrsima.f ⊢ φ → F Fn 𝒫 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 ⊢ φ → F B ∈ V
6 5 elexd ⊢ φ → F B ∈ V
7 isipodrs ⊢ toInc ⁡ B ∈ Dirset ↔ B ∈ V ∧ B ≠ ∅ ∧ ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B a ∪ b ⊆ c
8 3 7 sylib ⊢ φ → B ∈ V ∧ B ≠ ∅ ∧ ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B a ∪ b ⊆ c
9 8 simp2d ⊢ φ → B ≠ ∅
10 fnimaeq0 ⊢ F Fn 𝒫 A ∧ B ⊆ 𝒫 A → F B = ∅ ↔ B = ∅
11 1 4 10 syl2anc ⊢ φ → F B = ∅ ↔ B = ∅
12 11 necon3bid ⊢ φ → F B ≠ ∅ ↔ B ≠ ∅
13 9 12 mpbird ⊢ φ → F B ≠ ∅
14 8 simp3d ⊢ φ → ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B a ∪ 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 ∈ B a ∪ b ⊆ c → ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
58 57 ralimdva ⊢ φ ∧ a ∈ B → ∀ b ∈ B ∃ c ∈ B a ∪ b ⊆ c → ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
59 58 ralimdva ⊢ φ → ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B a ∪ b ⊆ c → ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
60 14 59 mpd ⊢ φ → ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B F ⁡ 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 ∈ F B x ∪ y ⊆ z ↔ ∃ z ∈ F B F ⁡ a ∪ y ⊆ z
64 63 ralbidv ⊢ x = F ⁡ a → ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z ↔ ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z
65 64 ralima ⊢ F Fn 𝒫 A ∧ B ⊆ 𝒫 A → ∀ x ∈ F B ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z ↔ ∀ a ∈ B ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z
66 1 4 65 syl2anc ⊢ φ → ∀ x ∈ F B ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z ↔ ∀ a ∈ B ∀ y ∈ F B ∃ z ∈ F B F ⁡ 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 ∈ F B F ⁡ a ∪ y ⊆ z ↔ ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z
70 69 ralima ⊢ F Fn 𝒫 A ∧ B ⊆ 𝒫 A → ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z ↔ ∀ b ∈ B ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z
71 1 4 70 syl2anc ⊢ φ → ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z ↔ ∀ b ∈ B ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z
72 sseq2 ⊢ z = F ⁡ c → F ⁡ a ∪ F ⁡ b ⊆ z ↔ F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
73 72 rexima ⊢ F Fn 𝒫 A ∧ B ⊆ 𝒫 A → ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z ↔ ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
74 1 4 73 syl2anc ⊢ φ → ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z ↔ ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
75 74 ralbidv ⊢ φ → ∀ b ∈ B ∃ z ∈ F B F ⁡ a ∪ F ⁡ b ⊆ z ↔ ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
76 71 75 bitrd ⊢ φ → ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z ↔ ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
77 76 ralbidv ⊢ φ → ∀ a ∈ B ∀ y ∈ F B ∃ z ∈ F B F ⁡ a ∪ y ⊆ z ↔ ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
78 66 77 bitrd ⊢ φ → ∀ x ∈ F B ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z ↔ ∀ a ∈ B ∀ b ∈ B ∃ c ∈ B F ⁡ a ∪ F ⁡ b ⊆ F ⁡ c
79 60 78 mpbird ⊢ φ → ∀ x ∈ F B ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z
80 isipodrs ⊢ toInc ⁡ F B ∈ Dirset ↔ F B ∈ V ∧ F B ≠ ∅ ∧ ∀ x ∈ F B ∀ y ∈ F B ∃ z ∈ F B x ∪ y ⊆ z
81 6 13 79 80 syl3anbrc ⊢ φ → toInc ⁡ F B ∈ Dirset