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 ⊢∀a∈𝒫A∀b∈𝒫Aa⊆b→F⁡a⊆F⁡b↔∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪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 ssun1 ⊢a⊆a∪b
11 simprl ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∈𝒫A
12 pwuncl ⊢a∈𝒫A∧b∈𝒫A→a∪b∈𝒫A
13 12 adantl ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a∪b∈𝒫A
14 simpl ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d
15 sseq1 ⊢c=a→c⊆d↔a⊆d
16 fveq2 ⊢c=a→F⁡c=F⁡a
17 16 sseq1d ⊢c=a→F⁡c⊆F⁡d↔F⁡a⊆F⁡d
18 15 17 imbi12d ⊢c=a→c⊆d→F⁡c⊆F⁡d↔a⊆d→F⁡a⊆F⁡d
19 sseq2 ⊢d=a∪b→a⊆d↔a⊆a∪b
20 fveq2 ⊢d=a∪b→F⁡d=F⁡a∪b
21 20 sseq2d ⊢d=a∪b→F⁡a⊆F⁡d↔F⁡a⊆F⁡a∪b
22 19 21 imbi12d ⊢d=a∪b→a⊆d→F⁡a⊆F⁡d↔a⊆a∪b→F⁡a⊆F⁡a∪b
23 18 22 rspc2va ⊢a∈𝒫A∧a∪b∈𝒫A∧∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→a⊆a∪b→F⁡a⊆F⁡a∪b
24 11 13 14 23 syl21anc ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→a⊆a∪b→F⁡a⊆F⁡a∪b
25 10 24 mpi ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡a⊆F⁡a∪b
26 ssun2 ⊢b⊆a∪b
27 simprr ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→b∈𝒫A
28 sseq1 ⊢c=b→c⊆d↔b⊆d
29 fveq2 ⊢c=b→F⁡c=F⁡b
30 29 sseq1d ⊢c=b→F⁡c⊆F⁡d↔F⁡b⊆F⁡d
31 28 30 imbi12d ⊢c=b→c⊆d→F⁡c⊆F⁡d↔b⊆d→F⁡b⊆F⁡d
32 sseq2 ⊢d=a∪b→b⊆d↔b⊆a∪b
33 20 sseq2d ⊢d=a∪b→F⁡b⊆F⁡d↔F⁡b⊆F⁡a∪b
34 32 33 imbi12d ⊢d=a∪b→b⊆d→F⁡b⊆F⁡d↔b⊆a∪b→F⁡b⊆F⁡a∪b
35 31 34 rspc2va ⊢b∈𝒫A∧a∪b∈𝒫A∧∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→b⊆a∪b→F⁡b⊆F⁡a∪b
36 27 13 14 35 syl21anc ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→b⊆a∪b→F⁡b⊆F⁡a∪b
37 26 36 mpi ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡b⊆F⁡a∪b
38 25 37 unssd ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d∧a∈𝒫A∧b∈𝒫A→F⁡a∪F⁡b⊆F⁡a∪b
39 38 ralrimivva ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d→∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b
40 ssequn1 ⊢c⊆d↔c∪d=d
41 2 uneq1d ⊢a=c→F⁡a∪F⁡b=F⁡c∪F⁡b
42 uneq1 ⊢a=c→a∪b=c∪b
43 42 fveq2d ⊢a=c→F⁡a∪b=F⁡c∪b
44 41 43 sseq12d ⊢a=c→F⁡a∪F⁡b⊆F⁡a∪b↔F⁡c∪F⁡b⊆F⁡c∪b
45 6 uneq2d ⊢b=d→F⁡c∪F⁡b=F⁡c∪F⁡d
46 uneq2 ⊢b=d→c∪b=c∪d
47 46 fveq2d ⊢b=d→F⁡c∪b=F⁡c∪d
48 45 47 sseq12d ⊢b=d→F⁡c∪F⁡b⊆F⁡c∪b↔F⁡c∪F⁡d⊆F⁡c∪d
49 44 48 rspc2va ⊢c∈𝒫A∧d∈𝒫A∧∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b→F⁡c∪F⁡d⊆F⁡c∪d
50 49 ancoms ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A→F⁡c∪F⁡d⊆F⁡c∪d
51 50 unssad ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A→F⁡c⊆F⁡c∪d
52 51 adantr ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A∧c∪d=d→F⁡c⊆F⁡c∪d
53 fveq2 ⊢c∪d=d→F⁡c∪d=F⁡d
54 53 adantl ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A∧c∪d=d→F⁡c∪d=F⁡d
55 52 54 sseqtrd ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A∧c∪d=d→F⁡c⊆F⁡d
56 55 ex ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A→c∪d=d→F⁡c⊆F⁡d
57 40 56 biimtrid ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b∧c∈𝒫A∧d∈𝒫A→c⊆d→F⁡c⊆F⁡d
58 57 ralrimivva ⊢∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b→∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d
59 39 58 impbii ⊢∀c∈𝒫A∀d∈𝒫Ac⊆d→F⁡c⊆F⁡d↔∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b
60 9 59 bitri ⊢∀a∈𝒫A∀b∈𝒫Aa⊆b→F⁡a⊆F⁡b↔∀a∈𝒫A∀b∈𝒫AF⁡a∪F⁡b⊆F⁡a∪b