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	syl5bi	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 → 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
30	5 29	impbid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )