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

Theorem isotone1 37366
 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 3589 . . . 4 (𝑎 = 𝑐 → (𝑎𝑏𝑐𝑏))
2 fveq2 6103 . . . . 5 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
32sseq1d 3595 . . . 4 (𝑎 = 𝑐 → ((𝐹𝑎) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑏)))
41, 3imbi12d 333 . . 3 (𝑎 = 𝑐 → ((𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ (𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏))))
5 sseq2 3590 . . . 4 (𝑏 = 𝑑 → (𝑐𝑏𝑐𝑑))
6 fveq2 6103 . . . . 5 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
76sseq2d 3596 . . . 4 (𝑏 = 𝑑 → ((𝐹𝑐) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑑)))
85, 7imbi12d 333 . . 3 (𝑏 = 𝑑 → ((𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏)) ↔ (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))))
94, 8cbvral2v 3155 . 2 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
10 ssun1 3738 . . . . . 6 𝑎 ⊆ (𝑎𝑏)
11 simprl 790 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12 elpwi 4117 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
1312adantr 480 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → 𝑎𝐴)
14 elpwi 4117 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝐴𝑏𝐴)
1514adantl 481 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → 𝑏𝐴)
1613, 15unssd 3751 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → (𝑎𝑏) ⊆ 𝐴)
17 vex 3176 . . . . . . . . . . 11 𝑎 ∈ V
18 vex 3176 . . . . . . . . . . 11 𝑏 ∈ V
1917, 18unex 6854 . . . . . . . . . 10 (𝑎𝑏) ∈ V
2019elpw 4114 . . . . . . . . 9 ((𝑎𝑏) ∈ 𝒫 𝐴 ↔ (𝑎𝑏) ⊆ 𝐴)
2116, 20sylibr 223 . . . . . . . 8 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → (𝑎𝑏) ∈ 𝒫 𝐴)
2221adantl 481 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎𝑏) ∈ 𝒫 𝐴)
23 simpl 472 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
24 sseq1 3589 . . . . . . . . 9 (𝑐 = 𝑎 → (𝑐𝑑𝑎𝑑))
25 fveq2 6103 . . . . . . . . . 10 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
2625sseq1d 3595 . . . . . . . . 9 (𝑐 = 𝑎 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹𝑑)))
2724, 26imbi12d 333 . . . . . . . 8 (𝑐 = 𝑎 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑))))
28 sseq2 3590 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑎𝑑𝑎 ⊆ (𝑎𝑏)))
29 fveq2 6103 . . . . . . . . . 10 (𝑑 = (𝑎𝑏) → (𝐹𝑑) = (𝐹‘(𝑎𝑏)))
3029sseq2d 3596 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑎) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3128, 30imbi12d 333 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑)) ↔ (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))))
3227, 31rspc2va 3294 . . . . . . 7 (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3311, 22, 23, 32syl21anc 1317 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3410, 33mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))
35 ssun2 3739 . . . . . 6 𝑏 ⊆ (𝑎𝑏)
36 simprr 792 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
37 sseq1 3589 . . . . . . . . 9 (𝑐 = 𝑏 → (𝑐𝑑𝑏𝑑))
38 fveq2 6103 . . . . . . . . . 10 (𝑐 = 𝑏 → (𝐹𝑐) = (𝐹𝑏))
3938sseq1d 3595 . . . . . . . . 9 (𝑐 = 𝑏 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹𝑑)))
4037, 39imbi12d 333 . . . . . . . 8 (𝑐 = 𝑏 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑))))
41 sseq2 3590 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑏𝑑𝑏 ⊆ (𝑎𝑏)))
4229sseq2d 3596 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑏) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4341, 42imbi12d 333 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑)) ↔ (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))))
4440, 43rspc2va 3294 . . . . . . 7 (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4536, 22, 23, 44syl21anc 1317 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4635, 45mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))
4734, 46unssd 3751 . . . 4 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
4847ralrimivva 2954 . . 3 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) → ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
49 ssequn1 3745 . . . . 5 (𝑐𝑑 ↔ (𝑐𝑑) = 𝑑)
502uneq1d 3728 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((𝐹𝑎) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑏)))
51 uneq1 3722 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
5251fveq2d 6107 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (𝐹‘(𝑎𝑏)) = (𝐹‘(𝑐𝑏)))
5350, 52sseq12d 3597 . . . . . . . . . . 11 (𝑎 = 𝑐 → (((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏))))
546uneq2d 3729 . . . . . . . . . . . 12 (𝑏 = 𝑑 → ((𝐹𝑐) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑑)))
55 uneq2 3723 . . . . . . . . . . . . 13 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
5655fveq2d 6107 . . . . . . . . . . . 12 (𝑏 = 𝑑 → (𝐹‘(𝑐𝑏)) = (𝐹‘(𝑐𝑑)))
5754, 56sseq12d 3597 . . . . . . . . . . 11 (𝑏 = 𝑑 → (((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑))))
5853, 57rspc2va 3294 . . . . . . . . . 10 (((𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏))) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
5958ancoms 468 . . . . . . . . 9 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
6059unssad 3752 . . . . . . . 8 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
6160adantr 480 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
62 fveq2 6103 . . . . . . . 8 ((𝑐𝑑) = 𝑑 → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
6362adantl 481 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
6461, 63sseqtrd 3604 . . . . . 6 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹𝑑))
6564ex 449 . . . . 5 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝑐𝑑) = 𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6649, 65syl5bi 231 . . . 4 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6766ralrimivva 2954 . . 3 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6848, 67impbii 198 . 2 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
699, 68bitri 263 1 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ∪ cun 3538   ⊆ wss 3540  𝒫 cpw 4108  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator