Step |
Hyp |
Ref |
Expression |
1 |
|
sseq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏 ) ) |
2 |
|
fveq2 |
⊢ ( 𝑎 = 𝑐 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) ) |
3 |
2
|
sseq1d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ) |
4 |
1 3
|
imbi12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝑐 ⊆ 𝑏 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ) ) |
5 |
|
sseq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑 ) ) |
6 |
|
fveq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑑 ) ) |
7 |
6
|
sseq2d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
8 |
5 7
|
imbi12d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 ⊆ 𝑏 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) ) |
9 |
4 8
|
cbvral2vw |
⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
10 |
|
ssun1 |
⊢ 𝑎 ⊆ ( 𝑎 ∪ 𝑏 ) |
11 |
|
simprl |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑎 ∈ 𝒫 𝐴 ) |
12 |
|
pwuncl |
⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 ) |
13 |
12
|
adantl |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 ) |
14 |
|
simpl |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
15 |
|
sseq1 |
⊢ ( 𝑐 = 𝑎 → ( 𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑 ) ) |
16 |
|
fveq2 |
⊢ ( 𝑐 = 𝑎 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑎 ) ) |
17 |
16
|
sseq1d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
18 |
15 17
|
imbi12d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( 𝑎 ⊆ 𝑑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) ) |
19 |
|
sseq2 |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( 𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ ( 𝑎 ∪ 𝑏 ) ) ) |
20 |
|
fveq2 |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
21 |
20
|
sseq2d |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
22 |
19 21
|
imbi12d |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝑎 ⊆ 𝑑 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( 𝑎 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) ) |
23 |
18 22
|
rspc2va |
⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) → ( 𝑎 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
24 |
11 13 14 23
|
syl21anc |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
25 |
10 24
|
mpi |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
26 |
|
ssun2 |
⊢ 𝑏 ⊆ ( 𝑎 ∪ 𝑏 ) |
27 |
|
simprr |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑏 ∈ 𝒫 𝐴 ) |
28 |
|
sseq1 |
⊢ ( 𝑐 = 𝑏 → ( 𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑 ) ) |
29 |
|
fveq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑏 ) ) |
30 |
29
|
sseq1d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
31 |
28 30
|
imbi12d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( 𝑏 ⊆ 𝑑 → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) ) |
32 |
|
sseq2 |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( 𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ ( 𝑎 ∪ 𝑏 ) ) ) |
33 |
20
|
sseq2d |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
34 |
32 33
|
imbi12d |
⊢ ( 𝑑 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝑏 ⊆ 𝑑 → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( 𝑏 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) ) |
35 |
31 34
|
rspc2va |
⊢ ( ( ( 𝑏 ∈ 𝒫 𝐴 ∧ ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) → ( 𝑏 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
36 |
27 13 14 35
|
syl21anc |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑏 ⊆ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) ) |
37 |
26 36
|
mpi |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
38 |
25 37
|
unssd |
⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
39 |
38
|
ralrimivva |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) → ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
40 |
|
ssequn1 |
⊢ ( 𝑐 ⊆ 𝑑 ↔ ( 𝑐 ∪ 𝑑 ) = 𝑑 ) |
41 |
2
|
uneq1d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ) |
42 |
|
uneq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∪ 𝑏 ) = ( 𝑐 ∪ 𝑏 ) ) |
43 |
42
|
fveq2d |
⊢ ( 𝑎 = 𝑐 → ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑐 ∪ 𝑏 ) ) ) |
44 |
41 43
|
sseq12d |
⊢ ( 𝑎 = 𝑐 → ( ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑏 ) ) ) ) |
45 |
6
|
uneq2d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑑 ) ) ) |
46 |
|
uneq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 ∪ 𝑏 ) = ( 𝑐 ∪ 𝑑 ) ) |
47 |
46
|
fveq2d |
⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ ( 𝑐 ∪ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) |
48 |
45 47
|
sseq12d |
⊢ ( 𝑏 = 𝑑 → ( ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑑 ) ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) ) |
49 |
44 48
|
rspc2va |
⊢ ( ( ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) → ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑑 ) ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) |
50 |
49
|
ancoms |
⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( ( 𝐹 ‘ 𝑐 ) ∪ ( 𝐹 ‘ 𝑑 ) ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) |
51 |
50
|
unssad |
⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) |
52 |
51
|
adantr |
⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ ( 𝑐 ∪ 𝑑 ) = 𝑑 ) → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) ) |
53 |
|
fveq2 |
⊢ ( ( 𝑐 ∪ 𝑑 ) = 𝑑 → ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) = ( 𝐹 ‘ 𝑑 ) ) |
54 |
53
|
adantl |
⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ ( 𝑐 ∪ 𝑑 ) = 𝑑 ) → ( 𝐹 ‘ ( 𝑐 ∪ 𝑑 ) ) = ( 𝐹 ‘ 𝑑 ) ) |
55 |
52 54
|
sseqtrd |
⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ ( 𝑐 ∪ 𝑑 ) = 𝑑 ) → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) |
56 |
55
|
ex |
⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( ( 𝑐 ∪ 𝑑 ) = 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
57 |
40 56
|
syl5bi |
⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
58 |
57
|
ralrimivva |
⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) → ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) |
59 |
39 58
|
impbii |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |
60 |
9 59
|
bitri |
⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ) |