Metamath Proof Explorer

Theorem suplub2

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

Ref Expression
Hypotheses supmo.1 ⊢ φ → R Or A
supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
suplub2.3 ⊢ φ → B ⊆ A
Assertion suplub2 ⊢ φ ∧ C ∈ A → C R sup B A R ↔ ∃ z ∈ B C R z

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ φ → R Or A
2 supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 suplub2.3 ⊢ φ → B ⊆ A
4 1 2 suplub ⊢ φ → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z
5 4 expdimp ⊢ φ ∧ C ∈ A → C R sup B A R → ∃ z ∈ B C R z
6 breq2 ⊢ z = w → C R z ↔ C R w
7 6 cbvrexvw ⊢ ∃ z ∈ B C R z ↔ ∃ w ∈ B C R w
8 breq2 ⊢ sup B A R = w → C R sup B A R ↔ C R w
9 8 biimprd ⊢ sup B A R = w → C R w → C R sup B A R
10 9 a1i ⊢ φ ∧ C ∈ A ∧ w ∈ B → sup B A R = w → C R w → C R sup B A R
11 1 ad2antrr ⊢ φ ∧ C ∈ A ∧ w ∈ B → R Or A
12 simplr ⊢ φ ∧ C ∈ A ∧ w ∈ B → C ∈ A
13 3 adantr ⊢ φ ∧ C ∈ A → B ⊆ A
14 13 sselda ⊢ φ ∧ C ∈ A ∧ w ∈ B → w ∈ A
15 1 2 supcl ⊢ φ → sup B A R ∈ A
16 15 ad2antrr ⊢ φ ∧ C ∈ A ∧ w ∈ B → sup B A R ∈ A
17 sotr ⊢ R Or A ∧ C ∈ A ∧ w ∈ A ∧ sup B A R ∈ A → C R w ∧ w R sup B A R → C R sup B A R
18 11 12 14 16 17 syl13anc ⊢ φ ∧ C ∈ A ∧ w ∈ B → C R w ∧ w R sup B A R → C R sup B A R
19 18 expcomd ⊢ φ ∧ C ∈ A ∧ w ∈ B → w R sup B A R → C R w → C R sup B A R
20 1 2 supub ⊢ φ → w ∈ B → ¬ sup B A R R w
21 20 adantr ⊢ φ ∧ C ∈ A → w ∈ B → ¬ sup B A R R w
22 21 imp ⊢ φ ∧ C ∈ A ∧ w ∈ B → ¬ sup B A R R w
23 sotric ⊢ R Or A ∧ sup B A R ∈ A ∧ w ∈ A → sup B A R R w ↔ ¬ sup B A R = w ∨ w R sup B A R
24 11 16 14 23 syl12anc ⊢ φ ∧ C ∈ A ∧ w ∈ B → sup B A R R w ↔ ¬ sup B A R = w ∨ w R sup B A R
25 24 con2bid ⊢ φ ∧ C ∈ A ∧ w ∈ B → sup B A R = w ∨ w R sup B A R ↔ ¬ sup B A R R w
26 22 25 mpbird ⊢ φ ∧ C ∈ A ∧ w ∈ B → sup B A R = w ∨ w R sup B A R
27 10 19 26 mpjaod ⊢ φ ∧ C ∈ A ∧ w ∈ B → C R w → C R sup B A R
28 27 rexlimdva ⊢ φ ∧ C ∈ A → ∃ w ∈ B C R w → C R sup B A R
29 7 28 syl5bi ⊢ φ ∧ C ∈ A → ∃ z ∈ B C R z → C R sup B A R
30 5 29 impbid ⊢ φ ∧ C ∈ A → C R sup B A R ↔ ∃ z ∈ B C R z