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 ⊢∀a∈𝒫A∀b∈𝒫Aa⊆b→F⁡a⊆F⁡b↔∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b

Proof

Step Hyp Ref Expression
1 sseq1 ⊢a=c→a⊆b↔c⊆b
2 fveq2 ⊢a=c→F⁡a=F⁡c
3 2 sseq1d ⊢a=c→F⁡a⊆F⁡b↔F⁡c⊆F⁡b
4 1 3 imbi12d ⊢a=c→a⊆b→F⁡a⊆F⁡b↔c⊆b→F⁡c⊆F⁡b
5 sseq2 ⊢b=d→c⊆b↔c⊆d
6 fveq2 ⊢b=d→F⁡b=F⁡d
7 6 sseq2d ⊢b=d→F⁡c⊆F⁡b↔F⁡c⊆F⁡d
8 5 7 imbi12d ⊢b=d→c⊆b→F⁡c⊆F⁡b↔c⊆d→F⁡c⊆F⁡d
9 4 8 cbvral2vw ⊢∀a∈𝒫A∀b∈𝒫Aa⊆b→F⁡a⊆F⁡b↔∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d
10 inss1 ⊢a∩b⊆a
11 inss2 ⊢a∩b⊆b
12 elpwi ⊢b∈𝒫A→b⊆A
13 11 12 sstrid ⊢b∈𝒫A→a∩b⊆A
14 vex ⊢b∈V
15 14 inex2 ⊢a∩b∈V
16 15 elpw ⊢a∩b∈𝒫A↔a∩b⊆A
17 13 16 sylibr ⊢b∈𝒫A→a∩b∈𝒫A
18 17 ad2antll ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∩b∈𝒫A
19 simprl ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∈𝒫A
20 simpl ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d
21 sseq1 ⊢c=a∩b→c⊆d↔a∩b⊆d
22 fveq2 ⊢c=a∩b→F⁡c=F⁡a∩b
23 22 sseq1d ⊢c=a∩b→F⁡c⊆F⁡d↔F⁡a∩b⊆F⁡d
24 21 23 imbi12d ⊢c=a∩b→c⊆d→F⁡c⊆F⁡d↔a∩b⊆d→F⁡a∩b⊆F⁡d
25 sseq2 ⊢d=a→a∩b⊆d↔a∩b⊆a
26 fveq2 ⊢d=a→F⁡d=F⁡a
27 26 sseq2d ⊢d=a→F⁡a∩b⊆F⁡d↔F⁡a∩b⊆F⁡a
28 25 27 imbi12d ⊢d=a→a∩b⊆d→F⁡a∩b⊆F⁡d↔a∩b⊆a→F⁡a∩b⊆F⁡a
29 24 28 rspc2va ⊢a∩b∈𝒫A∧a∈𝒫A∧∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→a∩b⊆a→F⁡a∩b⊆F⁡a
30 18 19 20 29 syl21anc ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∩b⊆a→F⁡a∩b⊆F⁡a
31 10 30 mpi ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡a∩b⊆F⁡a
32 simprr ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→b∈𝒫A
33 sseq2 ⊢d=b→a∩b⊆d↔a∩b⊆b
34 fveq2 ⊢d=b→F⁡d=F⁡b
35 34 sseq2d ⊢d=b→F⁡a∩b⊆F⁡d↔F⁡a∩b⊆F⁡b
36 33 35 imbi12d ⊢d=b→a∩b⊆d→F⁡a∩b⊆F⁡d↔a∩b⊆b→F⁡a∩b⊆F⁡b
37 24 36 rspc2va ⊢a∩b∈𝒫A∧b∈𝒫A∧∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→a∩b⊆b→F⁡a∩b⊆F⁡b
38 18 32 20 37 syl21anc ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∩b⊆b→F⁡a∩b⊆F⁡b
39 11 38 mpi ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡a∩b⊆F⁡b
40 31 39 ssind ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡a∩b⊆F⁡a∩F⁡b
41 40 ralrimivva ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b
42 dfss ⊢c⊆d↔c=c∩d
43 fveq2 ⊢c=c∩d→F⁡c=F⁡c∩d
44 43 adantl ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A∧c=c∩d→F⁡c=F⁡c∩d
45 ineq1 ⊢a=c→a∩b=c∩b
46 45 fveq2d ⊢a=c→F⁡a∩b=F⁡c∩b
47 2 ineq1d ⊢a=c→F⁡a∩F⁡b=F⁡c∩F⁡b
48 46 47 sseq12d ⊢a=c→F⁡a∩b⊆F⁡a∩F⁡b↔F⁡c∩b⊆F⁡c∩F⁡b
49 ineq2 ⊢b=d→c∩b=c∩d
50 49 fveq2d ⊢b=d→F⁡c∩b=F⁡c∩d
51 6 ineq2d ⊢b=d→F⁡c∩F⁡b=F⁡c∩F⁡d
52 50 51 sseq12d ⊢b=d→F⁡c∩b⊆F⁡c∩F⁡b↔F⁡c∩d⊆F⁡c∩F⁡d
53 48 52 rspc2va ⊢c∈𝒫A∧d∈𝒫A∧∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b→F⁡c∩d⊆F⁡c∩F⁡d
54 53 ancoms ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A→F⁡c∩d⊆F⁡c∩F⁡d
55 inss2 ⊢F⁡c∩F⁡d⊆F⁡d
56 54 55 sstrdi ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A→F⁡c∩d⊆F⁡d
57 56 adantr ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A∧c=c∩d→F⁡c∩d⊆F⁡d
58 44 57 eqsstrd ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A∧c=c∩d→F⁡c⊆F⁡d
59 58 ex ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A→c=c∩d→F⁡c⊆F⁡d
60 42 59 biimtrid ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b∧c∈𝒫A∧d∈𝒫A→c⊆d→F⁡c⊆F⁡d
61 60 ralrimivva ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b→∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d
62 41 61 impbii ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d↔∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b
63 9 62 bitri ⊢∀a∈𝒫A∀b∈𝒫Aa⊆b→F⁡a⊆F⁡b↔∀a∈𝒫A∀b∈𝒫AF⁡a∩b⊆F⁡a∩F⁡b