Metamath Proof Explorer

Theorem isotone2

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

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

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 inss1 ⊢ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎
11 inss2 ⊢ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑏
12 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴 )
13 11 12 sstrid ⊢ ( 𝑏 ∈ 𝒫 𝐴 → ( 𝑎 ∩ 𝑏 ) ⊆ 𝐴 )
14 vex ⊢ 𝑏 ∈ V
15 14 inex2 ⊢ ( 𝑎 ∩ 𝑏 ) ∈ V
16 15 elpw ⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐴 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝐴 )
17 13 16 sylibr ⊢ ( 𝑏 ∈ 𝒫 𝐴 → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐴 )
18 17 ad2antll ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐴 )
19 simprl ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑎 ∈ 𝒫 𝐴 )
20 simpl ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
21 sseq1 ⊢ ( 𝑐 = ( 𝑎 ∩ 𝑏 ) → ( 𝑐 ⊆ 𝑑 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 ) )
22 fveq2 ⊢ ( 𝑐 = ( 𝑎 ∩ 𝑏 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) )
23 22 sseq1d ⊢ ( 𝑐 = ( 𝑎 ∩ 𝑏 ) → ( ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
24 21 23 imbi12d ⊢ ( 𝑐 = ( 𝑎 ∩ 𝑏 ) → ( ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) )
25 sseq2 ⊢ ( 𝑑 = 𝑎 → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎 ) )
26 fveq2 ⊢ ( 𝑑 = 𝑎 → ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑎 ) )
27 26 sseq2d ⊢ ( 𝑑 = 𝑎 → ( ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) )
28 25 27 imbi12d ⊢ ( 𝑑 = 𝑎 → ( ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ) )
29 24 28 rspc2va ⊢ ( ( ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) )
30 18 19 20 29 syl21anc ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) ) )
31 10 30 mpi ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑎 ) )
32 simprr ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑏 ∈ 𝒫 𝐴 )
33 sseq2 ⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑏 ) )
34 fveq2 ⊢ ( 𝑑 = 𝑏 → ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝑏 ) )
35 34 sseq2d ⊢ ( 𝑑 = 𝑏 → ( ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ↔ ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
36 33 35 imbi12d ⊢ ( 𝑑 = 𝑏 → ( ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑑 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑏 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ) )
37 24 36 rspc2va ⊢ ( ( ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ) → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑏 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
38 18 32 20 37 syl21anc ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝑎 ∩ 𝑏 ) ⊆ 𝑏 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
39 11 38 mpi ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( 𝐹 ‘ 𝑏 ) )
40 31 39 ssind ⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) )
41 40 ralrimivva ⊢ ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) → ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) )
42 dfss ⊢ ( 𝑐 ⊆ 𝑑 ↔ 𝑐 = ( 𝑐 ∩ 𝑑 ) )
43 fveq2 ⊢ ( 𝑐 = ( 𝑐 ∩ 𝑑 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) )
44 43 adantl ⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ 𝑐 = ( 𝑐 ∩ 𝑑 ) ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) )
45 ineq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∩ 𝑏 ) = ( 𝑐 ∩ 𝑏 ) )
46 45 fveq2d ⊢ ( 𝑎 = 𝑐 → ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑐 ∩ 𝑏 ) ) )
47 2 ineq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑏 ) ) )
48 46 47 sseq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝐹 ‘ ( 𝑐 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ) )
49 ineq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 ∩ 𝑏 ) = ( 𝑐 ∩ 𝑑 ) )
50 49 fveq2d ⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ ( 𝑐 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) )
51 6 ineq2d ⊢ ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑑 ) ) )
52 50 51 sseq12d ⊢ ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ ( 𝑐 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) ⊆ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑑 ) ) ) )
53 48 52 rspc2va ⊢ ( ( ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ∧ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ) → ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) ⊆ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑑 ) ) )
54 53 ancoms ⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) ⊆ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑑 ) ) )
55 inss2 ⊢ ( ( 𝐹 ‘ 𝑐 ) ∩ ( 𝐹 ‘ 𝑑 ) ) ⊆ ( 𝐹 ‘ 𝑑 )
56 54 55 sstrdi ⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) )
57 56 adantr ⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ 𝑐 = ( 𝑐 ∩ 𝑑 ) ) → ( 𝐹 ‘ ( 𝑐 ∩ 𝑑 ) ) ⊆ ( 𝐹 ‘ 𝑑 ) )
58 44 57 eqsstrd ⊢ ( ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) ∧ 𝑐 = ( 𝑐 ∩ 𝑑 ) ) → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) )
59 58 ex ⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝑐 = ( 𝑐 ∩ 𝑑 ) → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
60 42 59 syl5bi ⊢ ( ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴 ) ) → ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
61 60 ralrimivva ⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) → ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) )
62 41 61 impbii ⊢ ( ∀ 𝑐 ∈ 𝒫 𝐴 ∀ 𝑑 ∈ 𝒫 𝐴 ( 𝑐 ⊆ 𝑑 → ( 𝐹 ‘ 𝑐 ) ⊆ ( 𝐹 ‘ 𝑑 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) )
63 9 62 bitri ⊢ ( ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 ⊆ 𝑏 → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝐹 ‘ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( ( 𝐹 ‘ 𝑎 ) ∩ ( 𝐹 ‘ 𝑏 ) ) )