Metamath Proof Explorer

Theorem ex-in

Description: Example for df-in . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ex-in 
|- ( { 1 , 3 } i^i { 1 , 8 } ) = { 1 }

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { 1 , 8 } = ( { 1 } u. { 8 } )
2 1 ineq2i 
 |-  ( { 1 , 3 } i^i { 1 , 8 } ) = ( { 1 , 3 } i^i ( { 1 } u. { 8 } ) )
3 indi 
 |-  ( { 1 , 3 } i^i ( { 1 } u. { 8 } ) ) = ( ( { 1 , 3 } i^i { 1 } ) u. ( { 1 , 3 } i^i { 8 } ) )
4 snsspr1 
 |-  { 1 } C_ { 1 , 3 }
5 sseqin2 
 |-  ( { 1 } C_ { 1 , 3 } <-> ( { 1 , 3 } i^i { 1 } ) = { 1 } )
6 4 5 mpbi 
 |-  ( { 1 , 3 } i^i { 1 } ) = { 1 }
7 1re 
 |-  1 e. RR
8 1lt8 
 |-  1 < 8
9 7 8 gtneii 
 |-  8 =/= 1
10 3re 
 |-  3 e. RR
11 3lt8 
 |-  3 < 8
12 10 11 gtneii 
 |-  8 =/= 3
13 9 12 nelpri 
 |-  -. 8 e. { 1 , 3 }
14 disjsn 
 |-  ( ( { 1 , 3 } i^i { 8 } ) = (/) <-> -. 8 e. { 1 , 3 } )
15 13 14 mpbir 
 |-  ( { 1 , 3 } i^i { 8 } ) = (/)
16 6 15 uneq12i 
 |-  ( ( { 1 , 3 } i^i { 1 } ) u. ( { 1 , 3 } i^i { 8 } ) ) = ( { 1 } u. (/) )
17 un0 
 |-  ( { 1 } u. (/) ) = { 1 }
18 16 17 eqtri 
 |-  ( ( { 1 , 3 } i^i { 1 } ) u. ( { 1 , 3 } i^i { 8 } ) ) = { 1 }
19 3 18 eqtri 
 |-  ( { 1 , 3 } i^i ( { 1 } u. { 8 } ) ) = { 1 }
20 2 19 eqtri 
 |-  ( { 1 , 3 } i^i { 1 , 8 } ) = { 1 }