Theorem supub

Description: A supremum is an upper bound. See also supcl and suplub .

This proof demonstrates how to expand an iota-based definition ( df-iota ) using riotacl2 .

(Contributed by NM, 12-Oct-2004) (Proof shortened by Mario Carneiro, 24-Dec-2016)

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

Proof

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