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

Theorem isotone1 37825
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 3605 . . . 4 (𝑎 = 𝑐 → (𝑎𝑏𝑐𝑏))
2 fveq2 6148 . . . . 5 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
32sseq1d 3611 . . . 4 (𝑎 = 𝑐 → ((𝐹𝑎) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑏)))
41, 3imbi12d 334 . . 3 (𝑎 = 𝑐 → ((𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ (𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏))))
5 sseq2 3606 . . . 4 (𝑏 = 𝑑 → (𝑐𝑏𝑐𝑑))
6 fveq2 6148 . . . . 5 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
76sseq2d 3612 . . . 4 (𝑏 = 𝑑 → ((𝐹𝑐) ⊆ (𝐹𝑏) ↔ (𝐹𝑐) ⊆ (𝐹𝑑)))
85, 7imbi12d 334 . . 3 (𝑏 = 𝑑 → ((𝑐𝑏 → (𝐹𝑐) ⊆ (𝐹𝑏)) ↔ (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))))
94, 8cbvral2v 3167 . 2 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
10 ssun1 3754 . . . . . 6 𝑎 ⊆ (𝑎𝑏)
11 simprl 793 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12 elpwi 4140 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
1312adantr 481 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → 𝑎𝐴)
14 elpwi 4140 . . . . . . . . . . 11 (𝑏 ∈ 𝒫 𝐴𝑏𝐴)
1514adantl 482 . . . . . . . . . 10 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → 𝑏𝐴)
1613, 15unssd 3767 . . . . . . . . 9 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → (𝑎𝑏) ⊆ 𝐴)
17 vex 3189 . . . . . . . . . . 11 𝑎 ∈ V
18 vex 3189 . . . . . . . . . . 11 𝑏 ∈ V
1917, 18unex 6909 . . . . . . . . . 10 (𝑎𝑏) ∈ V
2019elpw 4136 . . . . . . . . 9 ((𝑎𝑏) ∈ 𝒫 𝐴 ↔ (𝑎𝑏) ⊆ 𝐴)
2116, 20sylibr 224 . . . . . . . 8 ((𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴) → (𝑎𝑏) ∈ 𝒫 𝐴)
2221adantl 482 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎𝑏) ∈ 𝒫 𝐴)
23 simpl 473 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
24 sseq1 3605 . . . . . . . . 9 (𝑐 = 𝑎 → (𝑐𝑑𝑎𝑑))
25 fveq2 6148 . . . . . . . . . 10 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
2625sseq1d 3611 . . . . . . . . 9 (𝑐 = 𝑎 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹𝑑)))
2724, 26imbi12d 334 . . . . . . . 8 (𝑐 = 𝑎 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑))))
28 sseq2 3606 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑎𝑑𝑎 ⊆ (𝑎𝑏)))
29 fveq2 6148 . . . . . . . . . 10 (𝑑 = (𝑎𝑏) → (𝐹𝑑) = (𝐹‘(𝑎𝑏)))
3029sseq2d 3612 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑎) ⊆ (𝐹𝑑) ↔ (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3128, 30imbi12d 334 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑎𝑑 → (𝐹𝑎) ⊆ (𝐹𝑑)) ↔ (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))))
3227, 31rspc2va 3307 . . . . . . 7 (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3311, 22, 23, 32syl21anc 1322 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎𝑏) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏))))
3410, 33mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑎) ⊆ (𝐹‘(𝑎𝑏)))
35 ssun2 3755 . . . . . 6 𝑏 ⊆ (𝑎𝑏)
36 simprr 795 . . . . . . 7 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
37 sseq1 3605 . . . . . . . . 9 (𝑐 = 𝑏 → (𝑐𝑑𝑏𝑑))
38 fveq2 6148 . . . . . . . . . 10 (𝑐 = 𝑏 → (𝐹𝑐) = (𝐹𝑏))
3938sseq1d 3611 . . . . . . . . 9 (𝑐 = 𝑏 → ((𝐹𝑐) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹𝑑)))
4037, 39imbi12d 334 . . . . . . . 8 (𝑐 = 𝑏 → ((𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ (𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑))))
41 sseq2 3606 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → (𝑏𝑑𝑏 ⊆ (𝑎𝑏)))
4229sseq2d 3612 . . . . . . . . 9 (𝑑 = (𝑎𝑏) → ((𝐹𝑏) ⊆ (𝐹𝑑) ↔ (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4341, 42imbi12d 334 . . . . . . . 8 (𝑑 = (𝑎𝑏) → ((𝑏𝑑 → (𝐹𝑏) ⊆ (𝐹𝑑)) ↔ (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))))
4440, 43rspc2va 3307 . . . . . . 7 (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑))) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4536, 22, 23, 44syl21anc 1322 . . . . . 6 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎𝑏) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏))))
4635, 45mpi 20 . . . . 5 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑏) ⊆ (𝐹‘(𝑎𝑏)))
4734, 46unssd 3767 . . . 4 ((∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
4847ralrimivva 2965 . . 3 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) → ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
49 ssequn1 3761 . . . . 5 (𝑐𝑑 ↔ (𝑐𝑑) = 𝑑)
502uneq1d 3744 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((𝐹𝑎) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑏)))
51 uneq1 3738 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
5251fveq2d 6152 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (𝐹‘(𝑎𝑏)) = (𝐹‘(𝑐𝑏)))
5350, 52sseq12d 3613 . . . . . . . . . . 11 (𝑎 = 𝑐 → (((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏))))
546uneq2d 3745 . . . . . . . . . . . 12 (𝑏 = 𝑑 → ((𝐹𝑐) ∪ (𝐹𝑏)) = ((𝐹𝑐) ∪ (𝐹𝑑)))
55 uneq2 3739 . . . . . . . . . . . . 13 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
5655fveq2d 6152 . . . . . . . . . . . 12 (𝑏 = 𝑑 → (𝐹‘(𝑐𝑏)) = (𝐹‘(𝑐𝑑)))
5754, 56sseq12d 3613 . . . . . . . . . . 11 (𝑏 = 𝑑 → (((𝐹𝑐) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑐𝑏)) ↔ ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑))))
5853, 57rspc2va 3307 . . . . . . . . . 10 (((𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏))) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
5958ancoms 469 . . . . . . . . 9 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝐹𝑐) ∪ (𝐹𝑑)) ⊆ (𝐹‘(𝑐𝑑)))
6059unssad 3768 . . . . . . . 8 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
6160adantr 481 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹‘(𝑐𝑑)))
62 fveq2 6148 . . . . . . . 8 ((𝑐𝑑) = 𝑑 → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
6362adantl 482 . . . . . . 7 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹‘(𝑐𝑑)) = (𝐹𝑑))
6461, 63sseqtrd 3620 . . . . . 6 (((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐𝑑) = 𝑑) → (𝐹𝑐) ⊆ (𝐹𝑑))
6564ex 450 . . . . 5 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → ((𝑐𝑑) = 𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6649, 65syl5bi 232 . . . 4 ((∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴)) → (𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6766ralrimivva 2965 . . 3 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)) → ∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)))
6848, 67impbii 199 . 2 (∀𝑐 ∈ 𝒫 𝐴𝑑 ∈ 𝒫 𝐴(𝑐𝑑 → (𝐹𝑐) ⊆ (𝐹𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
699, 68bitri 264 1 (∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎𝑏 → (𝐹𝑎) ⊆ (𝐹𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴((𝐹𝑎) ∪ (𝐹𝑏)) ⊆ (𝐹‘(𝑎𝑏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  cun 3553  wss 3555  𝒫 cpw 4130  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator