| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > brtpos0 | Structured version Visualization version GIF version | ||
| Description: The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows to eliminate sethood hypotheses on 𝐴, 𝐵 in brtpos 8177. (Contributed by Mario Carneiro, 10-Sep-2015.) |
| Ref | Expression |
|---|---|
| brtpos0 | ⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brtpos2 8174 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ (∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴))) | |
| 2 | ssun2 4131 | . . . . 5 ⊢ {∅} ⊆ (◡dom 𝐹 ∪ {∅}) | |
| 3 | 0ex 5252 | . . . . . 6 ⊢ ∅ ∈ V | |
| 4 | 3 | snid 4619 | . . . . 5 ⊢ ∅ ∈ {∅} |
| 5 | 2, 4 | sselii 3930 | . . . 4 ⊢ ∅ ∈ (◡dom 𝐹 ∪ {∅}) |
| 6 | 5 | biantrur 530 | . . 3 ⊢ (∪ ◡{∅}𝐹𝐴 ↔ (∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴)) |
| 7 | cnvsn0 6168 | . . . . . 6 ⊢ ◡{∅} = ∅ | |
| 8 | 7 | unieqi 4875 | . . . . 5 ⊢ ∪ ◡{∅} = ∪ ∅ |
| 9 | uni0 4891 | . . . . 5 ⊢ ∪ ∅ = ∅ | |
| 10 | 8, 9 | eqtri 2759 | . . . 4 ⊢ ∪ ◡{∅} = ∅ |
| 11 | 10 | breq1i 5105 | . . 3 ⊢ (∪ ◡{∅}𝐹𝐴 ↔ ∅𝐹𝐴) |
| 12 | 6, 11 | bitr3i 277 | . 2 ⊢ ((∅ ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{∅}𝐹𝐴) ↔ ∅𝐹𝐴) |
| 13 | 1, 12 | bitrdi 287 | 1 ⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2113 ∪ cun 3899 ∅c0 4285 {csn 4580 ∪ cuni 4863 class class class wbr 5098 ◡ccnv 5623 dom cdm 5624 tpos ctpos 8167 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-fv 6500 df-tpos 8168 |
| This theorem is referenced by: reldmtpos 8176 brtpos 8177 tpostpos 8188 tposres0 49122 |
| Copyright terms: Public domain | W3C validator |