Theorem suplub

Description: A supremum is the least upper bound. See also supcl and supub . (Contributed by NM, 13-Oct-2004) (Revised by Mario Carneiro, 24-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		supmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		supcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
3		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑤 𝑅 𝑥 ) )
4		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑧 ↔ 𝑤 𝑅 𝑧 ) )
5	4	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
6	3 5	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
7	6	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
8	7	bilani	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
9	8	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
10	9	ss2rabi	⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) }
11	1	supval2	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) )
12	1 2	supeu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
13		riotacl2	⊢ ( ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
14	12 13	syl	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
15	11 14	eqeltrd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
16	10 15	sselid	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } )
17		breq2	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( 𝑤 𝑅 𝑥 ↔ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
18	17	imbi1d	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
19	18	ralbidv	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
20	19	elrab	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } ↔ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
21	20	simprbi	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
22	16 21	syl	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
23		breq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
24		breq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 𝑧 ↔ 𝐶 𝑅 𝑧 ) )
25	24	rexbidv	⊢ ( 𝑤 = 𝐶 → ( ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
26	23 25	imbi12d	⊢ ( 𝑤 = 𝐶 → ( ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
27	26	rspccv	⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
28	27	impd	⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
29	22 28	syl	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )