# Metamath Proof Explorer

## Theorem suplub2

Description: Bidirectional form of suplub . (Contributed by Mario Carneiro, 6-Sep-2014)

Ref Expression
Hypotheses supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
supcl.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$
suplub2.3 ${⊢}{\phi }\to {B}\subseteq {A}$
Assertion suplub2 ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left({C}{R}sup\left({B},{A},{R}\right)↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$

### Proof

Step Hyp Ref Expression
1 supmo.1 ${⊢}{\phi }\to {R}\mathrm{Or}{A}$
2 supcl.2 ${⊢}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$
3 suplub2.3 ${⊢}{\phi }\to {B}\subseteq {A}$
4 1 2 suplub ${⊢}{\phi }\to \left(\left({C}\in {A}\wedge {C}{R}sup\left({B},{A},{R}\right)\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$
5 4 expdimp ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left({C}{R}sup\left({B},{A},{R}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$
6 breq2 ${⊢}{z}={w}\to \left({C}{R}{z}↔{C}{R}{w}\right)$
7 6 cbvrexvw ${⊢}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{w}$
8 breq2 ${⊢}sup\left({B},{A},{R}\right)={w}\to \left({C}{R}sup\left({B},{A},{R}\right)↔{C}{R}{w}\right)$
9 8 biimprd ${⊢}sup\left({B},{A},{R}\right)={w}\to \left({C}{R}{w}\to {C}{R}sup\left({B},{A},{R}\right)\right)$
10 9 a1i ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left(sup\left({B},{A},{R}\right)={w}\to \left({C}{R}{w}\to {C}{R}sup\left({B},{A},{R}\right)\right)\right)$
11 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to {R}\mathrm{Or}{A}$
12 simplr ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to {C}\in {A}$
13 3 adantr ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to {B}\subseteq {A}$
14 13 sselda ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to {w}\in {A}$
15 1 2 supcl ${⊢}{\phi }\to sup\left({B},{A},{R}\right)\in {A}$
16 15 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to sup\left({B},{A},{R}\right)\in {A}$
17 sotr ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({C}\in {A}\wedge {w}\in {A}\wedge sup\left({B},{A},{R}\right)\in {A}\right)\right)\to \left(\left({C}{R}{w}\wedge {w}{R}sup\left({B},{A},{R}\right)\right)\to {C}{R}sup\left({B},{A},{R}\right)\right)$
18 11 12 14 16 17 syl13anc ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left(\left({C}{R}{w}\wedge {w}{R}sup\left({B},{A},{R}\right)\right)\to {C}{R}sup\left({B},{A},{R}\right)\right)$
19 18 expcomd ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left({w}{R}sup\left({B},{A},{R}\right)\to \left({C}{R}{w}\to {C}{R}sup\left({B},{A},{R}\right)\right)\right)$
20 1 2 supub ${⊢}{\phi }\to \left({w}\in {B}\to ¬sup\left({B},{A},{R}\right){R}{w}\right)$
21 20 adantr ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left({w}\in {B}\to ¬sup\left({B},{A},{R}\right){R}{w}\right)$
22 21 imp ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to ¬sup\left({B},{A},{R}\right){R}{w}$
23 sotric ${⊢}\left({R}\mathrm{Or}{A}\wedge \left(sup\left({B},{A},{R}\right)\in {A}\wedge {w}\in {A}\right)\right)\to \left(sup\left({B},{A},{R}\right){R}{w}↔¬\left(sup\left({B},{A},{R}\right)={w}\vee {w}{R}sup\left({B},{A},{R}\right)\right)\right)$
24 11 16 14 23 syl12anc ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left(sup\left({B},{A},{R}\right){R}{w}↔¬\left(sup\left({B},{A},{R}\right)={w}\vee {w}{R}sup\left({B},{A},{R}\right)\right)\right)$
25 24 con2bid ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left(\left(sup\left({B},{A},{R}\right)={w}\vee {w}{R}sup\left({B},{A},{R}\right)\right)↔¬sup\left({B},{A},{R}\right){R}{w}\right)$
26 22 25 mpbird ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left(sup\left({B},{A},{R}\right)={w}\vee {w}{R}sup\left({B},{A},{R}\right)\right)$
27 10 19 26 mpjaod ${⊢}\left(\left({\phi }\wedge {C}\in {A}\right)\wedge {w}\in {B}\right)\to \left({C}{R}{w}\to {C}{R}sup\left({B},{A},{R}\right)\right)$
28 27 rexlimdva ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{w}\to {C}{R}sup\left({B},{A},{R}\right)\right)$
29 7 28 syl5bi ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\to {C}{R}sup\left({B},{A},{R}\right)\right)$
30 5 29 impbid ${⊢}\left({\phi }\wedge {C}\in {A}\right)\to \left({C}{R}sup\left({B},{A},{R}\right)↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{C}{R}{z}\right)$