Metamath Proof Explorer


Theorem pimgtmnf

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -oo , is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimgtmnf.1 x φ
pimgtmnf.2 φ x A B
Assertion pimgtmnf φ x A | −∞ < B = A

Proof

Step Hyp Ref Expression
1 pimgtmnf.1 x φ
2 pimgtmnf.2 φ x A B
3 eqidd φ x A B = x A B
4 3 2 fvmpt2d φ x A x A B x = B
5 4 eqcomd φ x A B = x A B x
6 5 breq2d φ x A −∞ < B −∞ < x A B x
7 1 6 rabbida φ x A | −∞ < B = x A | −∞ < x A B x
8 nfmpt1 _ x x A B
9 eqid x A B = x A B
10 1 2 9 fmptdf φ x A B : A
11 8 10 pimgtmnf2 φ x A | −∞ < x A B x = A
12 7 11 eqtrd φ x A | −∞ < B = A