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 ( ∀ 𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴 ( 𝑎𝑏 → ( 𝐹𝑎 ) ⊆ ( 𝐹𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴 ( ( 𝐹𝑎 ) ∪ ( 𝐹𝑏 ) ) ⊆ ( 𝐹 ‘ ( 𝑎𝑏 ) ) )

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