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 ⊢ ( 𝜑 → 𝐹 Fn 𝒫 𝐴 )
ipodrsima.m ⊢ ( ( 𝜑 ∧ ( 𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴 ) ) → ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) )
ipodrsima.d ⊢ ( 𝜑 → ( toInc ‘ 𝐵 ) ∈ Dirset )
ipodrsima.s ⊢ ( 𝜑 → 𝐵 ⊆ 𝒫 𝐴 )
ipodrsima.a ⊢ ( 𝜑 → ( 𝐹 “ 𝐵 ) ∈ 𝑉 )
Assertion ipodrsima ( 𝜑 → ( toInc ‘ ( 𝐹 “ 𝐵 ) ) ∈ Dirset )

Proof

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