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 ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d
10 ssun1 ⊢ a ⊆ a ∪ b
11 simprl ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ 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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ∪ b ∈ 𝒫 A
14 simpl ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ 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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → a ⊆ a ∪ b → F ⁡ a ⊆ F ⁡ a ∪ b
24 11 13 14 23 syl21anc ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ⊆ a ∪ b → F ⁡ a ⊆ F ⁡ a ∪ b
25 10 24 mpi ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ a ⊆ F ⁡ a ∪ b
26 ssun2 ⊢ b ⊆ a ∪ b
27 simprr ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ 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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → b ⊆ a ∪ b → F ⁡ b ⊆ F ⁡ a ∪ b
36 27 13 14 35 syl21anc ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → b ⊆ a ∪ b → F ⁡ b ⊆ F ⁡ a ∪ b
37 26 36 mpi ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ b ⊆ F ⁡ a ∪ b
38 25 37 unssd ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b
39 38 ralrimivva ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b → F ⁡ c ∪ F ⁡ d ⊆ F ⁡ c ∪ d
50 49 ancoms ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → F ⁡ c ∪ F ⁡ d ⊆ F ⁡ c ∪ d
51 50 unssad ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → F ⁡ c ⊆ F ⁡ c ∪ d
52 51 adantr ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A ∧ c ∪ d = d → F ⁡ c ⊆ F ⁡ d
56 55 ex ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → c ∪ d = d → F ⁡ c ⊆ F ⁡ d
57 40 56 syl5bi ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → c ⊆ d → F ⁡ c ⊆ F ⁡ d
58 57 ralrimivva ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b → ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d
59 39 58 impbii ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b
60 9 59 bitri ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∪ F ⁡ b ⊆ F ⁡ a ∪ b