This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suplub2

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

Ref Expression
Hypotheses supmo.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
supcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
suplub2.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion suplub2 ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 supcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
3 suplub2.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4 1 2 suplub ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
5 4 expdimp ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
6 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐶 𝑅 𝑧 ↔ 𝐶 𝑅 𝑤 ) )
7 6 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ↔ ∃ 𝑤 ∈ 𝐵 𝐶 𝑅 𝑤 )
8 breq2 ⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ 𝐶 𝑅 𝑤 ) )
9 8 biimprd ⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 → ( 𝐶 𝑅 𝑤 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
10 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 → ( 𝐶 𝑅 𝑤 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
11 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑅 Or 𝐴 )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝐶 ∈ 𝐴 )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ⊆ 𝐴 )
14 13 sselda ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐴 )
15 1 2 supcl ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
17 sotr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ) ) → ( ( 𝐶 𝑅 𝑤 ∧ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
18 11 12 14 16 17 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝐶 𝑅 𝑤 ∧ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
19 18 expcomd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ( 𝐶 𝑅 𝑤 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
20 1 2 supub ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐵 → ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑤 ∈ 𝐵 → ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 ) )
22 21 imp ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 )
23 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 ↔ ¬ ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 ∨ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
24 11 16 14 23 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 ↔ ¬ ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 ∨ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
25 24 con2bid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 ∨ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝑤 ) )
26 22 25 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝑤 ∨ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
27 10 19 26 mpjaod ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝐶 𝑅 𝑤 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
28 27 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑤 ∈ 𝐵 𝐶 𝑅 𝑤 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
29 7 28 biimtrid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
30 5 29 impbid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )