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		simpr	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
4		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑤 𝑅 𝑥 ) )
5		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑧 ↔ 𝑤 𝑅 𝑧 ) )
6	5	rexbidv	⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
7	4 6	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
8	7	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
9	3 8	sylib	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
10	9	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
11	10	ss2rabi	⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) }
12	1	supval2	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) )
13	1 2	supeu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
14		riotacl2	⊢ ( ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
15	13 14	syl	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
16	12 15	eqeltrd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
17	11 16	sseldi	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } )
18		breq2	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( 𝑤 𝑅 𝑥 ↔ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
19	18	imbi1d	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
20	19	ralbidv	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
21	20	elrab	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } ↔ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
22	21	simprbi	⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
23	17 22	syl	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
24		breq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
25		breq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 𝑧 ↔ 𝐶 𝑅 𝑧 ) )
26	25	rexbidv	⊢ ( 𝑤 = 𝐶 → ( ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
27	24 26	imbi12d	⊢ ( 𝑤 = 𝐶 → ( ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
28	27	rspccv	⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
29	28	impd	⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
30	23 29	syl	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )