Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isotone1 Structured version   Visualization version   GIF version

Theorem isotone1 41124
 Description: Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)
Assertion
Ref Expression
isotone1 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
Distinct variable groups:   𝐴,𝑎,𝑏   𝐹,𝑎,𝑏

Proof of Theorem isotone1
Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3917 . . . 4 (𝑎 = 𝑐 → (𝑎𝑏𝑐𝑏))
2 fveq2 6658 . . . . 5 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
32sseq1d 3923 . . . 4 (𝑎 = 𝑐 → ((𝐹𝑎) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑏)))
41, 3imbi12d 348 . . 3 (𝑎 = 𝑐 → ((𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ (𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏))))
5 sseq2 3918 . . . 4 (𝑏 = 𝑑 → (𝑐𝑏𝑐𝑑))
6 fveq2 6658 . . . . 5 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
76sseq2d 3924 . . . 4 (𝑏 = 𝑑 → ((𝐹𝑐) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑑)))
85, 7imbi12d 348 . . 3 (𝑏 = 𝑑 → ((𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏)) ↔ (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))))
94, 8cbvral2vw 3373 . 2 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
10 ssun1 4077 . . . . . 6 𝑎 ⊆ (𝑎𝑏)
11 simprl 770 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12 pwuncl 7491 . . . . . . . 8 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → (𝑎𝑏) ∈ 𝒫 𝐴)
1312adantl 485 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎𝑏) ∈ 𝒫 𝐴)
14 simpl 486 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
15 sseq1 3917 . . . . . . . . 9 (𝑐 = 𝑎 → (𝑐𝑑𝑎𝑑))
16 fveq2 6658 . . . . . . . . . 10 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
1716sseq1d 3923 . . . . . . . . 9 (𝑐 = 𝑎 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹𝑑)))
1815, 17imbi12d 348 . . . . . . . 8 (𝑐 = 𝑎 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑))))
19 sseq2 3918 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑎𝑑𝑎 ⊆ (𝑎𝑏)))
20 fveq2 6658 . . . . . . . . . 10 (𝑑 = (𝑎𝑏) → (𝐹𝑑) = (𝐹‘(𝑎𝑏)))
2120sseq2d 3924 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑎) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
2219, 21imbi12d 348 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑)) ↔ (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))))
2318, 22rspc2va 3552 . . . . . . 7 (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
2411, 13, 14, 23syl21anc 836 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
2510, 24mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))
26 ssun2 4078 . . . . . 6 𝑏 ⊆ (𝑎𝑏)
27 simprr 772 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28 sseq1 3917 . . . . . . . . 9 (𝑐 = 𝑏 → (𝑐𝑑𝑏𝑑))
29 fveq2 6658 . . . . . . . . . 10 (𝑐 = 𝑏 → (𝐹𝑐) = (𝐹𝑏))
3029sseq1d 3923 . . . . . . . . 9 (𝑐 = 𝑏 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹𝑑)))
3128, 30imbi12d 348 . . . . . . . 8 (𝑐 = 𝑏 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑))))
32 sseq2 3918 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑏𝑑𝑏 ⊆ (𝑎𝑏)))
3320sseq2d 3924 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑏) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
3432, 33imbi12d 348 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑)) ↔ (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))))
3531, 34rspc2va 3552 . . . . . . 7 (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
3627, 13, 14, 35syl21anc 836 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
3726, 36mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))
3825, 37unssd 4091 . . . 4 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
3938ralrimivva 3120 . . 3 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) → ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
40 ssequn1 4085 . . . . 5 (𝑐𝑑 ↔ (𝑐𝑑) = 𝑑)
412uneq1d 4067 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((𝐹𝑎) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑏)))
42 uneq1 4061 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
4342fveq2d 6662 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (𝐹‘(𝑎𝑏)) = (𝐹‘(𝑐𝑏)))
4441, 43sseq12d 3925 . . . . . . . . . . 11 (𝑎 = 𝑐 → (((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏))))
456uneq2d 4068 . . . . . . . . . . . 12 (𝑏 = 𝑑 → ((𝐹𝑐) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑑)))
46 uneq2 4062 . . . . . . . . . . . . 13 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
4746fveq2d 6662 . . . . . . . . . . . 12 (𝑏 = 𝑑 → (𝐹‘(𝑐𝑏)) = (𝐹‘(𝑐𝑑)))
4845, 47sseq12d 3925 . . . . . . . . . . 11 (𝑏 = 𝑑 → (((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑))))
4944, 48rspc2va 3552 . . . . . . . . . 10 (((𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏))) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
5049ancoms 462 . . . . . . . . 9 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
5150unssad 4092 . . . . . . . 8 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
5251adantr 484 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
53 fveq2 6658 . . . . . . . 8 ((𝑐𝑑) = 𝑑 → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
5453adantl 485 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
5552, 54sseqtrd 3932 . . . . . 6 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹𝑑))
5655ex 416 . . . . 5 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝑐𝑑) = 𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
5740, 56syl5bi 245 . . . 4 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
5857ralrimivva 3120 . . 3 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
5939, 58impbii 212 . 2 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
609, 59bitri 278 1 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070   ∪ cun 3856   ⊆ wss 3858  𝒫 cpw 4494  ‘cfv 6335 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rab 3079  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator