Metamath Proof Explorer

Theorem isotone1

Description: Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021)

Ref Expression
Assertion isotone1 ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) )

Proof

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 biimtrid ⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
58 57 ralrimivva ⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) → ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
59 39 58 impbii ⊢ ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) )
60 9 59 bitri ⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( ( 𝐹 ‘ 𝑎 ) ∪ ( 𝐹 ‘ 𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎 ∪ 𝑏 ) ) )