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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
2 | 1 | elint | |
3 | vex | |
|
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 | |