Step | Hyp | Ref
| Expression |
1 | | djulf1o 7057 |
. . . . . . . . 9
ā¢
inl:Vā1-1-ontoā({ā
} Ć V) |
2 | | f1of1 5461 |
. . . . . . . . 9
ā¢
(inl:Vā1-1-ontoā({ā
} Ć V) ā inl:Vā1-1ā({ā
} Ć V)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
ā¢
inl:Vā1-1ā({ā
}
Ć V) |
4 | | ssv 3178 |
. . . . . . . 8
ā¢ š“ ā V |
5 | | f1ores 5477 |
. . . . . . . 8
ā¢
((inl:Vā1-1ā({ā
}
Ć V) ā§ š“ ā
V) ā (inl ā¾ š“):š“ā1-1-ontoā(inl
ā š“)) |
6 | 3, 4, 5 | mp2an 426 |
. . . . . . 7
ā¢ (inl
ā¾ š“):š“ā1-1-ontoā(inl
ā š“) |
7 | | f1oeng 6757 |
. . . . . . 7
ā¢ ((š“ ā š ā§ (inl ā¾ š“):š“ā1-1-ontoā(inl
ā š“)) ā š“ ā (inl ā š“)) |
8 | 6, 7 | mpan2 425 |
. . . . . 6
ā¢ (š“ ā š ā š“ ā (inl ā š“)) |
9 | 8 | ensymd 6783 |
. . . . 5
ā¢ (š“ ā š ā (inl ā š“) ā š“) |
10 | | djurf1o 7058 |
. . . . . . . 8
ā¢
inr:Vā1-1-ontoā({1o} Ć V) |
11 | | f1of1 5461 |
. . . . . . . 8
ā¢
(inr:Vā1-1-ontoā({1o} Ć V) ā
inr:Vā1-1ā({1o}
Ć V)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
ā¢
inr:Vā1-1ā({1o} Ć V) |
13 | | f1ores 5477 |
. . . . . . 7
ā¢
((inr:Vā1-1ā({1o} Ć V) ā§ š“ ā V) ā (inr ā¾
š“):š“ā1-1-ontoā(inr
ā š“)) |
14 | 12, 4, 13 | mp2an 426 |
. . . . . 6
ā¢ (inr
ā¾ š“):š“ā1-1-ontoā(inr
ā š“) |
15 | | f1oeng 6757 |
. . . . . 6
ā¢ ((š“ ā š ā§ (inr ā¾ š“):š“ā1-1-ontoā(inr
ā š“)) ā š“ ā (inr ā š“)) |
16 | 14, 15 | mpan2 425 |
. . . . 5
ā¢ (š“ ā š ā š“ ā (inr ā š“)) |
17 | | entr 6784 |
. . . . 5
ā¢ (((inl
ā š“) ā š“ ā§ š“ ā (inr ā š“)) ā (inl ā š“) ā (inr ā š“)) |
18 | 9, 16, 17 | syl2anc 411 |
. . . 4
ā¢ (š“ ā š ā (inl ā š“) ā (inr ā š“)) |
19 | 18 | adantr 276 |
. . 3
ā¢ ((š“ ā š ā§ šµ ā š) ā (inl ā š“) ā (inr ā š“)) |
20 | | ssv 3178 |
. . . . . . . 8
ā¢ šµ ā V |
21 | | f1ores 5477 |
. . . . . . . 8
ā¢
((inr:Vā1-1ā({1o} Ć V) ā§ šµ ā V) ā (inr ā¾
šµ):šµā1-1-ontoā(inr
ā šµ)) |
22 | 12, 20, 21 | mp2an 426 |
. . . . . . 7
ā¢ (inr
ā¾ šµ):šµā1-1-ontoā(inr
ā šµ) |
23 | | f1oeng 6757 |
. . . . . . 7
ā¢ ((šµ ā š ā§ (inr ā¾ šµ):šµā1-1-ontoā(inr
ā šµ)) ā šµ ā (inr ā šµ)) |
24 | 22, 23 | mpan2 425 |
. . . . . 6
ā¢ (šµ ā š ā šµ ā (inr ā šµ)) |
25 | 24 | adantl 277 |
. . . . 5
ā¢ ((š“ ā š ā§ šµ ā š) ā šµ ā (inr ā šµ)) |
26 | 25 | ensymd 6783 |
. . . 4
ā¢ ((š“ ā š ā§ šµ ā š) ā (inr ā šµ) ā šµ) |
27 | | f1ores 5477 |
. . . . . . 7
ā¢
((inl:Vā1-1ā({ā
}
Ć V) ā§ šµ ā
V) ā (inl ā¾ šµ):šµā1-1-ontoā(inl
ā šµ)) |
28 | 3, 20, 27 | mp2an 426 |
. . . . . 6
ā¢ (inl
ā¾ šµ):šµā1-1-ontoā(inl
ā šµ) |
29 | | f1oeng 6757 |
. . . . . 6
ā¢ ((šµ ā š ā§ (inl ā¾ šµ):šµā1-1-ontoā(inl
ā šµ)) ā šµ ā (inl ā šµ)) |
30 | 28, 29 | mpan2 425 |
. . . . 5
ā¢ (šµ ā š ā šµ ā (inl ā šµ)) |
31 | 30 | adantl 277 |
. . . 4
ā¢ ((š“ ā š ā§ šµ ā š) ā šµ ā (inl ā šµ)) |
32 | | entr 6784 |
. . . 4
ā¢ (((inr
ā šµ) ā šµ ā§ šµ ā (inl ā šµ)) ā (inr ā šµ) ā (inl ā šµ)) |
33 | 26, 31, 32 | syl2anc 411 |
. . 3
ā¢ ((š“ ā š ā§ šµ ā š) ā (inr ā šµ) ā (inl ā šµ)) |
34 | | djuin 7063 |
. . . 4
ā¢ ((inl
ā š“) ā© (inr
ā šµ)) =
ā
|
35 | 34 | a1i 9 |
. . 3
ā¢ ((š“ ā š ā§ šµ ā š) ā ((inl ā š“) ā© (inr ā šµ)) = ā
) |
36 | | incom 3328 |
. . . . 5
ā¢ ((inl
ā šµ) ā© (inr
ā š“)) = ((inr ā
š“) ā© (inl ā šµ)) |
37 | | djuin 7063 |
. . . . 5
ā¢ ((inl
ā šµ) ā© (inr
ā š“)) =
ā
|
38 | 36, 37 | eqtr3i 2200 |
. . . 4
ā¢ ((inr
ā š“) ā© (inl
ā šµ)) =
ā
|
39 | 38 | a1i 9 |
. . 3
ā¢ ((š“ ā š ā§ šµ ā š) ā ((inr ā š“) ā© (inl ā šµ)) = ā
) |
40 | | unen 6816 |
. . 3
ā¢ ((((inl
ā š“) ā (inr
ā š“) ā§ (inr
ā šµ) ā (inl
ā šµ)) ā§ (((inl
ā š“) ā© (inr
ā šµ)) = ā
ā§
((inr ā š“) ā© (inl
ā šµ)) = ā
))
ā ((inl ā š“)
āŖ (inr ā šµ))
ā ((inr ā š“)
āŖ (inl ā šµ))) |
41 | 19, 33, 35, 39, 40 | syl22anc 1239 |
. 2
ā¢ ((š“ ā š ā§ šµ ā š) ā ((inl ā š“) āŖ (inr ā šµ)) ā ((inr ā š“) āŖ (inl ā šµ))) |
42 | | djuun 7066 |
. 2
ā¢ ((inl
ā š“) āŖ (inr
ā šµ)) = (š“ ā šµ) |
43 | | uncom 3280 |
. . 3
ā¢ ((inr
ā š“) āŖ (inl
ā šµ)) = ((inl ā
šµ) āŖ (inr ā š“)) |
44 | | djuun 7066 |
. . 3
ā¢ ((inl
ā šµ) āŖ (inr
ā š“)) = (šµ ā š“) |
45 | 43, 44 | eqtri 2198 |
. 2
ā¢ ((inr
ā š“) āŖ (inl
ā šµ)) = (šµ ā š“) |
46 | 41, 42, 45 | 3brtr3g 4037 |
1
ā¢ ((š“ ā š ā§ šµ ā š) ā (š“ ā šµ) ā (šµ ā š“)) |