Metamath Proof Explorer


Theorem elixx3g

Description: Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR* . (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypothesis ixx.1 O = x * , y * z * | x R z z S y
Assertion elixx3g C A O B A * B * C * A R C C S B

Proof

Step Hyp Ref Expression
1 ixx.1 O = x * , y * z * | x R z z S y
2 anass A * B * C * A R C C S B A * B * C * A R C C S B
3 df-3an A * B * C * A * B * C *
4 3 anbi1i A * B * C * A R C C S B A * B * C * A R C C S B
5 1 elixx1 A * B * C A O B C * A R C C S B
6 3anass C * A R C C S B C * A R C C S B
7 ibar A * B * C * A R C C S B A * B * C * A R C C S B
8 6 7 syl5bb A * B * C * A R C C S B A * B * C * A R C C S B
9 5 8 bitrd A * B * C A O B A * B * C * A R C C S B
10 1 ixxf O : * × * 𝒫 *
11 10 fdmi dom O = * × *
12 11 ndmov ¬ A * B * A O B =
13 12 eleq2d ¬ A * B * C A O B C
14 noel ¬ C
15 14 pm2.21i C A * B *
16 simpl A * B * C * A R C C S B A * B *
17 15 16 pm5.21ni ¬ A * B * C A * B * C * A R C C S B
18 13 17 bitrd ¬ A * B * C A O B A * B * C * A R C C S B
19 9 18 pm2.61i C A O B A * B * C * A R C C S B
20 2 4 19 3bitr4ri C A O B A * B * C * A R C C S B