![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvun | Structured version Visualization version GIF version |
Description: The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
cnvun | ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-cnv 5645 | . . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} | |
2 | unopab 5191 | . . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} | |
3 | brun 5160 | . . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
4 | 3 | opabbii 5176 | . . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} |
5 | 2, 4 | eqtr4i 2764 | . . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} |
6 | 1, 5 | eqtr4i 2764 | . 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) |
7 | df-cnv 5645 | . . 3 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} | |
8 | df-cnv 5645 | . . 3 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥} | |
9 | 7, 8 | uneq12i 4125 | . 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) |
10 | 6, 9 | eqtr4i 2764 | 1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 846 = wceq 1542 ∪ cun 3912 class class class wbr 5109 {copab 5171 ◡ccnv 5636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3449 df-un 3919 df-br 5110 df-opab 5172 df-cnv 5645 |
This theorem is referenced by: rnun 6102 funcnvpr 6567 funcnvtp 6568 funcnvqp 6569 f1oun 6807 f1oprswap 6832 suppun 8119 sbthlem8 9040 domss2 9086 cnvfi 9130 1sdomOLD 9199 fsuppun 9332 fpwwe2lem12 10586 trclublem 14889 mbfres2 25032 ex-cnv 29430 cnvprop 31664 padct 31690 cycpmconjslem2 32060 eulerpartlemt 33035 mthmpps 34240 clcnvlem 41987 frege131d 42128 |
Copyright terms: Public domain | W3C validator |