Theorem intprg

Description: The intersection of a pair is the intersection of its members. Closed form of intpr . Theorem 71 of Suppes p. 42. (Contributed by FL, 27-Apr-2008) (Proof shortened by BJ, 1-Sep-2024)

	Ref	Expression
Assertion	intprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elint	⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) )
3		vex	⊢ 𝑦 ∈ V
4	3	elpr	⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
5	4	imbi1i	⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) )
6		jaob	⊢ ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
7	5 6	bitri	⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
8	7	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑦 ) ↔ ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
9		19.26	⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
10	2 8 9	3bitri	⊢ ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
11		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
12		clel4g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↔ ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ) )
13		clel4g	⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐵 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) )
14	12 13	bi2anan9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ) )
15	11 14	bitr2id	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ∀ 𝑦 ( 𝑦 = 𝐴 → 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝑥 ∈ 𝑦 ) ) ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
16	10 15	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
17	16	alrimiv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑥 ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
18		dfcleq	⊢ ( ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∩ { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
19	17 18	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )