Step | Hyp | Ref
| Expression |
1 | | incom 4166 |
. 2
ā¢ ((inr
ā šµ) ā© (inl
ā š“)) = ((inl ā
š“) ā© (inr ā šµ)) |
2 | | imassrn 6029 |
. . . 4
ā¢ (inr
ā šµ) ā ran
inr |
3 | | djurf1o 9856 |
. . . . 5
ā¢
inr:Vā1-1-ontoā({1o} Ć V) |
4 | | f1of 6789 |
. . . . 5
ā¢
(inr:Vā1-1-ontoā({1o} Ć V) ā
inr:Vā¶({1o} Ć V)) |
5 | | frn 6680 |
. . . . 5
ā¢
(inr:Vā¶({1o} Ć V) ā ran inr ā
({1o} Ć V)) |
6 | 3, 4, 5 | mp2b 10 |
. . . 4
ā¢ ran inr
ā ({1o} Ć V) |
7 | 2, 6 | sstri 3958 |
. . 3
ā¢ (inr
ā šµ) ā
({1o} Ć V) |
8 | | incom 4166 |
. . . 4
ā¢ ((inl
ā š“) ā©
({1o} Ć V)) = (({1o} Ć V) ā© (inl ā
š“)) |
9 | | imassrn 6029 |
. . . . . 6
ā¢ (inl
ā š“) ā ran
inl |
10 | | djulf1o 9855 |
. . . . . . 7
ā¢
inl:Vā1-1-ontoā({ā
} Ć V) |
11 | | f1of 6789 |
. . . . . . 7
ā¢
(inl:Vā1-1-ontoā({ā
} Ć V) ā
inl:Vā¶({ā
} Ć V)) |
12 | | frn 6680 |
. . . . . . 7
ā¢
(inl:Vā¶({ā
} Ć V) ā ran inl ā ({ā
}
Ć V)) |
13 | 10, 11, 12 | mp2b 10 |
. . . . . 6
ā¢ ran inl
ā ({ā
} Ć V) |
14 | 9, 13 | sstri 3958 |
. . . . 5
ā¢ (inl
ā š“) ā
({ā
} Ć V) |
15 | | 1n0 8439 |
. . . . . . 7
ā¢
1o ā ā
|
16 | 15 | necomi 2999 |
. . . . . 6
ā¢ ā
ā 1o |
17 | | disjsn2 4678 |
. . . . . 6
ā¢ (ā
ā 1o ā ({ā
} ā© {1o}) =
ā
) |
18 | | xpdisj1 6118 |
. . . . . 6
ā¢
(({ā
} ā© {1o}) = ā
ā (({ā
} Ć
V) ā© ({1o} Ć V)) = ā
) |
19 | 16, 17, 18 | mp2b 10 |
. . . . 5
ā¢
(({ā
} Ć V) ā© ({1o} Ć V)) =
ā
|
20 | | ssdisj 4424 |
. . . . 5
ā¢ (((inl
ā š“) ā
({ā
} Ć V) ā§ (({ā
} Ć V) ā© ({1o}
Ć V)) = ā
) ā ((inl ā š“) ā© ({1o} Ć V)) =
ā
) |
21 | 14, 19, 20 | mp2an 691 |
. . . 4
ā¢ ((inl
ā š“) ā©
({1o} Ć V)) = ā
|
22 | 8, 21 | eqtr3i 2767 |
. . 3
ā¢
(({1o} Ć V) ā© (inl ā š“)) = ā
|
23 | | ssdisj 4424 |
. . 3
ā¢ (((inr
ā šµ) ā
({1o} Ć V) ā§ (({1o} Ć V) ā© (inl
ā š“)) = ā
)
ā ((inr ā šµ)
ā© (inl ā š“)) =
ā
) |
24 | 7, 22, 23 | mp2an 691 |
. 2
ā¢ ((inr
ā šµ) ā© (inl
ā š“)) =
ā
|
25 | 1, 24 | eqtr3i 2767 |
1
ā¢ ((inl
ā š“) ā© (inr
ā šµ)) =
ā
|