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 ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ 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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ∩ b ∈ 𝒫 A
19 simprl ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ∈ 𝒫 A
20 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
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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → a ∩ b ⊆ a → F ⁡ a ∩ b ⊆ F ⁡ a
30 18 19 20 29 syl21anc ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ∩ b ⊆ a → F ⁡ a ∩ b ⊆ F ⁡ a
31 10 30 mpi ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ a ∩ b ⊆ F ⁡ a
32 simprr ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ 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 ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → a ∩ b ⊆ b → F ⁡ a ∩ b ⊆ F ⁡ b
38 18 32 20 37 syl21anc ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → a ∩ b ⊆ b → F ⁡ a ∩ b ⊆ F ⁡ b
39 11 38 mpi ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ a ∩ b ⊆ F ⁡ b
40 31 39 ssind ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ∧ a ∈ 𝒫 A ∧ b ∈ 𝒫 A → F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b
41 40 ralrimivva ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d → ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b → F ⁡ c ∩ d ⊆ F ⁡ c ∩ F ⁡ d
54 53 ancoms ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → F ⁡ c ∩ d ⊆ F ⁡ d
57 56 adantr ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ 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 ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A ∧ c = c ∩ d → F ⁡ c ⊆ F ⁡ d
59 58 ex ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → c = c ∩ d → F ⁡ c ⊆ F ⁡ d
60 42 59 biimtrid ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b ∧ c ∈ 𝒫 A ∧ d ∈ 𝒫 A → c ⊆ d → F ⁡ c ⊆ F ⁡ d
61 60 ralrimivva ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b → ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d
62 41 61 impbii ⊢ ∀ c ∈ 𝒫 A ∀ d ∈ 𝒫 A c ⊆ d → F ⁡ c ⊆ F ⁡ d ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b
63 9 62 bitri ⊢ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A a ⊆ b → F ⁡ a ⊆ F ⁡ b ↔ ∀ a ∈ 𝒫 A ∀ b ∈ 𝒫 A F ⁡ a ∩ b ⊆ F ⁡ a ∩ F ⁡ b