This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfif5

Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false (see also ab0orv ). (Contributed by Gérard Lang, 18-Aug-2013)

Ref Expression
Hypothesis dfif3.1 ⊢ 𝐶 = { 𝑥 ∣ 𝜑 }
Assertion dfif5 if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfif3.1 ⊢ 𝐶 = { 𝑥 ∣ 𝜑 }
2 inindi ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) ) = ( ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) ∩ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) )
3 1 dfif4 ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) )
4 undir ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( 𝐴 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) ∩ ( 𝐵 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) )
5 unidm ⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
6 5 uneq1i ⊢ ( ( 𝐴 ∪ 𝐴 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) )
7 unass ⊢ ( ( 𝐴 ∪ 𝐴 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∪ ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) )
8 undi ⊢ ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) )
9 6 7 8 3eqtr3ri ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∪ ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) )
10 undi ⊢ ( 𝐴 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) = ( ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) ∩ ( 𝐴 ∪ 𝐶 ) )
11 undifabs ⊢ ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
12 11 ineq1i ⊢ ( ( 𝐴 ∪ ( 𝐴 ∖ 𝐵 ) ) ∩ ( 𝐴 ∪ 𝐶 ) ) = ( 𝐴 ∩ ( 𝐴 ∪ 𝐶 ) )
13 inabs ⊢ ( 𝐴 ∩ ( 𝐴 ∪ 𝐶 ) ) = 𝐴
14 10 12 13 3eqtri ⊢ ( 𝐴 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) = 𝐴
15 undif2 ⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
16 15 ineq1i ⊢ ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) )
17 undi ⊢ ( 𝐴 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) )
18 16 17 8 3eqtr4i ⊢ ( 𝐴 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) )
19 14 18 uneq12i ⊢ ( ( 𝐴 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐴 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) = ( 𝐴 ∪ ( 𝐴 ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) )
20 9 19 eqtr4i ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐴 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
21 unundi ⊢ ( 𝐴 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( 𝐴 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐴 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
22 20 21 eqtr4i ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
23 unass ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) ∪ 𝐵 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∪ 𝐵 ) )
24 undi ⊢ ( 𝐵 ∪ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐵 ∪ 𝐴 ) ∩ ( 𝐵 ∪ 𝐶 ) )
25 uncom ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( 𝐴 ∩ 𝐶 ) )
26 undif2 ⊢ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐵 ∪ 𝐴 )
27 26 ineq1i ⊢ ( ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐵 ∪ 𝐴 ) ∩ ( 𝐵 ∪ 𝐶 ) )
28 24 25 27 3eqtr4i ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) = ( ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ∩ ( 𝐵 ∪ 𝐶 ) )
29 undi ⊢ ( 𝐵 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) = ( ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ∩ ( 𝐵 ∪ 𝐶 ) )
30 28 29 eqtr4i ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) )
31 undi ⊢ ( 𝐵 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐵 ∪ ( 𝐵 ∖ 𝐴 ) ) ∩ ( 𝐵 ∪ ( V ∖ 𝐶 ) ) )
32 undifabs ⊢ ( 𝐵 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
33 32 ineq1i ⊢ ( ( 𝐵 ∪ ( 𝐵 ∖ 𝐴 ) ) ∩ ( 𝐵 ∪ ( V ∖ 𝐶 ) ) ) = ( 𝐵 ∩ ( 𝐵 ∪ ( V ∖ 𝐶 ) ) )
34 inabs ⊢ ( 𝐵 ∩ ( 𝐵 ∪ ( V ∖ 𝐶 ) ) ) = 𝐵
35 31 33 34 3eqtrri ⊢ 𝐵 = ( 𝐵 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) )
36 30 35 uneq12i ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) ∪ 𝐵 ) = ( ( 𝐵 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐵 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
37 unidm ⊢ ( 𝐵 ∪ 𝐵 ) = 𝐵
38 37 uneq2i ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∪ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 )
39 23 36 38 3eqtr3ri ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) = ( ( 𝐵 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐵 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
40 uncom ⊢ ( 𝐵 ∪ 𝐶 ) = ( 𝐶 ∪ 𝐵 )
41 40 ineq2i ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐶 ∪ 𝐵 ) )
42 undir ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐶 ∪ 𝐵 ) )
43 41 42 eqtr4i ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ 𝐵 )
44 unundi ⊢ ( 𝐵 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( 𝐵 ∪ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ) ∪ ( 𝐵 ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
45 39 43 44 3eqtr4i ⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐵 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )
46 22 45 ineq12i ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) ∩ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) ) = ( ( 𝐴 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) ∩ ( 𝐵 ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) )
47 4 46 eqtr4i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) ) = ( ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ ( V ∖ 𝐶 ) ) ) ∩ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐵 ∪ 𝐶 ) ) )
48 2 3 47 3eqtr4i ⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∪ ( ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐶 ) ∪ ( ( 𝐵 ∖ 𝐴 ) ∩ ( V ∖ 𝐶 ) ) ) )