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	biimpri	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
6	5	adantl	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
7		sseq2	⊢ ( 𝑧 = 𝐶 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝐶 ) )
8		simpll	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ 𝐵 )
9		simplr	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐴 ⊆ 𝐶 )
10	7 8 9	elrabd	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } )
11		sseq2	⊢ ( 𝑧 = 𝑥 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑥 ) )
12	11	cbvrabv	⊢ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } = { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
13	10 12	eleqtrdi	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
14		intss1	⊢ ( 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
15	13 14	syl	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
16	6 15	eqssd	⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
17	16	expl	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
18		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
19		sseq2	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ↔ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
20	18 19	mpbiri	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐴 ⊆ 𝐶 )
21		eqimss	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
22	21 4	sylib	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
23	20 22	jca	⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) )
24	17 23	impbid1	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) ↔ 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )