| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nrex1 | Structured version Visualization version GIF version | ||
| Description: The class of signed reals is a set. Note that a shorter proof is possible using qsex 8754 (and not requiring enrer 11021), but it would add a dependency on ax-rep 5227. (Contributed by Mario Carneiro, 17-Nov-2014.) Extract proof from that of axcnex 11105. (Revised by BJ, 4-Feb-2023.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| nrex1 | ⊢ R ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nr 11014 | . 2 ⊢ R = ((P × P) / ~R ) | |
| 2 | npex 10944 | . . . . 5 ⊢ P ∈ V | |
| 3 | 2, 2 | xpex 7736 | . . . 4 ⊢ (P × P) ∈ V |
| 4 | 3 | pwex 5337 | . . 3 ⊢ 𝒫 (P × P) ∈ V |
| 5 | enrer 11021 | . . . . . 6 ⊢ ~R Er (P × P) | |
| 6 | 5 | a1i 11 | . . . . 5 ⊢ (⊤ → ~R Er (P × P)) |
| 7 | 6 | qsss 8757 | . . . 4 ⊢ (⊤ → ((P × P) / ~R ) ⊆ 𝒫 (P × P)) |
| 8 | 7 | mptru 1567 | . . 3 ⊢ ((P × P) / ~R ) ⊆ 𝒫 (P × P) |
| 9 | 4, 8 | ssexi 5278 | . 2 ⊢ ((P × P) / ~R ) ∈ V |
| 10 | 1, 9 | eqeltri 2858 | 1 ⊢ R ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ⊤wtru 1561 ∈ wcel 2142 Vcvv 3454 ⊆ wss 3904 𝒫 cpw 4555 × cxp 5645 Er wer 8675 / cqs 8677 Pcnp 10817 ~R cer 10822 Rcnr 10823 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-oadd 8441 df-omul 8442 df-er 8678 df-ec 8680 df-qs 8684 df-ni 10830 df-pli 10831 df-mi 10832 df-lti 10833 df-plpq 10866 df-mpq 10867 df-ltpq 10868 df-enq 10869 df-nq 10870 df-erq 10871 df-plq 10872 df-mq 10873 df-1nq 10874 df-rq 10875 df-ltnq 10876 df-np 10939 df-plp 10941 df-ltp 10943 df-enr 11013 df-nr 11014 |
| This theorem is referenced by: axcnex 11105 bj-inftyexpitaudisj 37694 |
| Copyright terms: Public domain | W3C validator |