Step | Hyp | Ref
| Expression |
1 | | neq0 4309 |
. . . . . . 7
β’ (Β¬
π₯ = β
β
βπ¦ π¦ β π₯) |
2 | | indistop 22375 |
. . . . . . . . . . 11
β’ {β
,
π΄} β
Top |
3 | | indistop 22375 |
. . . . . . . . . . 11
β’ {β
,
π΅} β
Top |
4 | | eltx 22942 |
. . . . . . . . . . 11
β’
(({β
, π΄}
β Top β§ {β
, π΅} β Top) β (π₯ β ({β
, π΄} Γt {β
, π΅}) β βπ¦ β π₯ βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯))) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . . . . . 10
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β βπ¦ β π₯ βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) |
6 | | rsp 3229 |
. . . . . . . . . 10
β’
(βπ¦ β
π₯ βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯) β (π¦ β π₯ β βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯))) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . 9
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (π¦ β π₯ β βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯))) |
8 | | elssuni 4902 |
. . . . . . . . . . . . . 14
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β π₯ β βͺ ({β
, π΄} Γt {β
, π΅})) |
9 | | indisuni 22376 |
. . . . . . . . . . . . . . 15
β’ ( I
βπ΄) = βͺ {β
, π΄} |
10 | | indisuni 22376 |
. . . . . . . . . . . . . . 15
β’ ( I
βπ΅) = βͺ {β
, π΅} |
11 | 2, 3, 9, 10 | txunii 22967 |
. . . . . . . . . . . . . 14
β’ (( I
βπ΄) Γ ( I
βπ΅)) = βͺ ({β
, π΄} Γt {β
, π΅}) |
12 | 8, 11 | sseqtrrdi 3999 |
. . . . . . . . . . . . 13
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β π₯ β (( I βπ΄) Γ ( I βπ΅))) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π₯ β ({β
, π΄} Γt {β
,
π΅}) β§ (π§ β {β
, π΄} β§ π€ β {β
, π΅})) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π₯ β (( I βπ΄) Γ ( I βπ΅))) |
14 | | ne0i 4298 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π§ Γ π€) β (π§ Γ π€) β β
) |
15 | 14 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π§ Γ π€) β β
) |
16 | | xpnz 6115 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ β β
β§ π€ β β
) β (π§ Γ π€) β β
) |
17 | 15, 16 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π§ β β
β§ π€ β β
)) |
18 | 17 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π§ β β
) |
19 | 18 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β Β¬ π§ = β
) |
20 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π§ β {β
, π΄}) |
21 | | indislem 22373 |
. . . . . . . . . . . . . . . . . . 19
β’ {β
,
( I βπ΄)} = {β
,
π΄} |
22 | 20, 21 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . 18
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π§ β {β
, ( I βπ΄)}) |
23 | | elpri 4612 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {β
, ( I
βπ΄)} β (π§ = β
β¨ π§ = ( I βπ΄))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π§ = β
β¨ π§ = ( I βπ΄))) |
25 | 24 | ord 863 |
. . . . . . . . . . . . . . . 16
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (Β¬ π§ = β
β π§ = ( I βπ΄))) |
26 | 19, 25 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π§ = ( I βπ΄)) |
27 | 17 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π€ β β
) |
28 | 27 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β Β¬ π€ = β
) |
29 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π€ β {β
, π΅}) |
30 | | indislem 22373 |
. . . . . . . . . . . . . . . . . . 19
β’ {β
,
( I βπ΅)} = {β
,
π΅} |
31 | 29, 30 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . 18
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π€ β {β
, ( I βπ΅)}) |
32 | | elpri 4612 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {β
, ( I
βπ΅)} β (π€ = β
β¨ π€ = ( I βπ΅))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π€ = β
β¨ π€ = ( I βπ΅))) |
34 | 33 | ord 863 |
. . . . . . . . . . . . . . . 16
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (Β¬ π€ = β
β π€ = ( I βπ΅))) |
35 | 28, 34 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π€ = ( I βπ΅)) |
36 | 26, 35 | xpeq12d 5668 |
. . . . . . . . . . . . . 14
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π§ Γ π€) = (( I βπ΄) Γ ( I βπ΅))) |
37 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (π§ Γ π€) β π₯) |
38 | 36, 37 | eqsstrrd 3987 |
. . . . . . . . . . . . 13
β’ (((π§ β {β
, π΄} β§ π€ β {β
, π΅}) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (( I βπ΄) Γ ( I βπ΅)) β π₯) |
39 | 38 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π₯ β ({β
, π΄} Γt {β
,
π΅}) β§ (π§ β {β
, π΄} β§ π€ β {β
, π΅})) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β (( I βπ΄) Γ ( I βπ΅)) β π₯) |
40 | 13, 39 | eqssd 3965 |
. . . . . . . . . . 11
β’ (((π₯ β ({β
, π΄} Γt {β
,
π΅}) β§ (π§ β {β
, π΄} β§ π€ β {β
, π΅})) β§ (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯)) β π₯ = (( I βπ΄) Γ ( I βπ΅))) |
41 | 40 | ex 414 |
. . . . . . . . . 10
β’ ((π₯ β ({β
, π΄} Γt {β
,
π΅}) β§ (π§ β {β
, π΄} β§ π€ β {β
, π΅})) β ((π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯) β π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
42 | 41 | rexlimdvva 3202 |
. . . . . . . . 9
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (βπ§ β {β
, π΄}βπ€ β {β
, π΅} (π¦ β (π§ Γ π€) β§ (π§ Γ π€) β π₯) β π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
43 | 7, 42 | syld 47 |
. . . . . . . 8
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (π¦ β π₯ β π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
44 | 43 | exlimdv 1937 |
. . . . . . 7
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (βπ¦ π¦ β π₯ β π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
45 | 1, 44 | biimtrid 241 |
. . . . . 6
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (Β¬ π₯ = β
β π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
46 | 45 | orrd 862 |
. . . . 5
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β (π₯ = β
β¨ π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
47 | | vex 3451 |
. . . . . 6
β’ π₯ β V |
48 | 47 | elpr 4613 |
. . . . 5
β’ (π₯ β {β
, (( I
βπ΄) Γ ( I
βπ΅))} β (π₯ = β
β¨ π₯ = (( I βπ΄) Γ ( I βπ΅)))) |
49 | 46, 48 | sylibr 233 |
. . . 4
β’ (π₯ β ({β
, π΄} Γt {β
,
π΅}) β π₯ β {β
, (( I
βπ΄) Γ ( I
βπ΅))}) |
50 | 49 | ssriv 3952 |
. . 3
β’
({β
, π΄}
Γt {β
, π΅}) β {β
, (( I βπ΄) Γ ( I βπ΅))} |
51 | 9 | toptopon 22289 |
. . . . . . 7
β’
({β
, π΄} β
Top β {β
, π΄}
β (TopOnβ( I βπ΄))) |
52 | 2, 51 | mpbi 229 |
. . . . . 6
β’ {β
,
π΄} β (TopOnβ( I
βπ΄)) |
53 | 10 | toptopon 22289 |
. . . . . . 7
β’
({β
, π΅} β
Top β {β
, π΅}
β (TopOnβ( I βπ΅))) |
54 | 3, 53 | mpbi 229 |
. . . . . 6
β’ {β
,
π΅} β (TopOnβ( I
βπ΅)) |
55 | | txtopon 22965 |
. . . . . 6
β’
(({β
, π΄}
β (TopOnβ( I βπ΄)) β§ {β
, π΅} β (TopOnβ( I βπ΅))) β ({β
, π΄} Γt {β
,
π΅}) β (TopOnβ((
I βπ΄) Γ ( I
βπ΅)))) |
56 | 52, 54, 55 | mp2an 691 |
. . . . 5
β’
({β
, π΄}
Γt {β
, π΅}) β (TopOnβ(( I βπ΄) Γ ( I βπ΅))) |
57 | | topgele 22302 |
. . . . 5
β’
(({β
, π΄}
Γt {β
, π΅}) β (TopOnβ(( I βπ΄) Γ ( I βπ΅))) β ({β
, (( I
βπ΄) Γ ( I
βπ΅))} β
({β
, π΄}
Γt {β
, π΅}) β§ ({β
, π΄} Γt {β
, π΅}) β π« (( I
βπ΄) Γ ( I
βπ΅)))) |
58 | 56, 57 | ax-mp 5 |
. . . 4
β’
({β
, (( I βπ΄) Γ ( I βπ΅))} β ({β
, π΄} Γt {β
, π΅}) β§ ({β
, π΄} Γt {β
,
π΅}) β π« (( I
βπ΄) Γ ( I
βπ΅))) |
59 | 58 | simpli 485 |
. . 3
β’ {β
,
(( I βπ΄) Γ ( I
βπ΅))} β
({β
, π΄}
Γt {β
, π΅}) |
60 | 50, 59 | eqssi 3964 |
. 2
β’
({β
, π΄}
Γt {β
, π΅}) = {β
, (( I βπ΄) Γ ( I βπ΅))} |
61 | | txindislem 23007 |
. . 3
β’ (( I
βπ΄) Γ ( I
βπ΅)) = ( I
β(π΄ Γ π΅)) |
62 | 61 | preq2i 4702 |
. 2
β’ {β
,
(( I βπ΄) Γ ( I
βπ΅))} = {β
, ( I
β(π΄ Γ π΅))} |
63 | | indislem 22373 |
. 2
β’ {β
,
( I β(π΄ Γ π΅))} = {β
, (π΄ Γ π΅)} |
64 | 60, 62, 63 | 3eqtri 2765 |
1
β’
({β
, π΄}
Γt {β
, π΅}) = {β
, (π΄ Γ π΅)} |