Theorem intubeu

Description: Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024)

	Ref	Expression
Assertion	intubeu	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) ↔ 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		ssint	⊢ ( 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } 𝐶 ⊆ 𝑦 )
2		sseq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦 ) )
3	2	ralrab	⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } 𝐶 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
4	1 3	bitri	⊢ ( 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
5	4	bilanri	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
6		sseq2	⊢ ( 𝑧 = 𝐶 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝐶 ) )
7		simpll	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ 𝐵 )
8		simplr	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐴 ⊆ 𝐶 )
9	6 7 8	elrabd	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } )
10		sseq2	⊢ ( 𝑧 = 𝑥 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑥 ) )
11	10	cbvrabv	⊢ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } = { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
12	9 11	eleqtrdi	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
13		intss1	⊢ ( 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
14	12 13	syl	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
15	5 14	eqssd	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
16	15	expl	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
17		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
18		sseq2	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ↔ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
19	17 18	mpbiri	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐴 ⊆ 𝐶 )
20		eqimss	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
21	20 4	sylib	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
22	19 21	jca	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) )
23	16 22	impbid1	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) ↔ 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )