Step | Hyp | Ref
| Expression |
1 | | incom 4194 |
. 2
⢠((inr
ā šµ) ā© (inl
ā š“)) = ((inl ā
š“) ā© (inr ā šµ)) |
2 | | imassrn 6061 |
. . . 4
⢠(inr
ā šµ) ā ran
inr |
3 | | djurf1o 9905 |
. . . . 5
ā¢
inr:Vā1-1-ontoā({1o} Ć V) |
4 | | f1of 6824 |
. . . . 5
ā¢
(inr:Vā1-1-ontoā({1o} Ć V) ā
inr:Vā¶({1o} Ć V)) |
5 | | frn 6715 |
. . . . 5
ā¢
(inr:Vā¶({1o} Ć V) ā ran inr ā
({1o} Ć V)) |
6 | 3, 4, 5 | mp2b 10 |
. . . 4
⢠ran inr
ā ({1o} Ć V) |
7 | 2, 6 | sstri 3984 |
. . 3
⢠(inr
ā šµ) ā
({1o} Ć V) |
8 | | incom 4194 |
. . . 4
⢠((inl
ā š“) ā©
({1o} Ć V)) = (({1o} Ć V) ā© (inl ā
š“)) |
9 | | imassrn 6061 |
. . . . . 6
⢠(inl
ā š“) ā ran
inl |
10 | | djulf1o 9904 |
. . . . . . 7
ā¢
inl:Vā1-1-ontoā({ā
} Ć V) |
11 | | f1of 6824 |
. . . . . . 7
ā¢
(inl:Vā1-1-ontoā({ā
} Ć V) ā
inl:Vā¶({ā
} Ć V)) |
12 | | frn 6715 |
. . . . . . 7
ā¢
(inl:Vā¶({ā
} Ć V) ā ran inl ā ({ā
}
Ć V)) |
13 | 10, 11, 12 | mp2b 10 |
. . . . . 6
⢠ran inl
ā ({ā
} Ć V) |
14 | 9, 13 | sstri 3984 |
. . . . 5
⢠(inl
ā š“) ā
({ā
} Ć V) |
15 | | 1n0 8484 |
. . . . . . 7
ā¢
1o ā ā
|
16 | 15 | necomi 2987 |
. . . . . 6
⢠ā
ā 1o |
17 | | disjsn2 4709 |
. . . . . 6
⢠(ā
ā 1o ā ({ā
} ā© {1o}) =
ā
) |
18 | | xpdisj1 6151 |
. . . . . 6
ā¢
(({ā
} ā© {1o}) = ā
ā (({ā
} Ć
V) ā© ({1o} Ć V)) = ā
) |
19 | 16, 17, 18 | mp2b 10 |
. . . . 5
ā¢
(({ā
} Ć V) ā© ({1o} Ć V)) =
ā
|
20 | | ssdisj 4452 |
. . . . 5
⢠(((inl
ā š“) ā
({ā
} Ć V) ā§ (({ā
} Ć V) ā© ({1o}
Ć V)) = ā
) ā ((inl ā š“) ā© ({1o} Ć V)) =
ā
) |
21 | 14, 19, 20 | mp2an 689 |
. . . 4
⢠((inl
ā š“) ā©
({1o} Ć V)) = ā
|
22 | 8, 21 | eqtr3i 2754 |
. . 3
ā¢
(({1o} Ć V) ā© (inl ā š“)) = ā
|
23 | | ssdisj 4452 |
. . 3
⢠(((inr
ā šµ) ā
({1o} Ć V) ā§ (({1o} Ć V) ā© (inl
ā š“)) = ā
)
ā ((inr ā šµ)
ā© (inl ā š“)) =
ā
) |
24 | 7, 22, 23 | mp2an 689 |
. 2
⢠((inr
ā šµ) ā© (inl
ā š“)) =
ā
|
25 | 1, 24 | eqtr3i 2754 |
1
⢠((inl
ā š“) ā© (inr
ā šµ)) =
ā
|