Step | Hyp | Ref
| Expression |
1 | | neq0 4279 |
. . . . . . 7
⊢ (¬
𝑥 = ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
2 | | indistop 22152 |
. . . . . . . . . . 11
⊢ {∅,
𝐴} ∈
Top |
3 | | indistop 22152 |
. . . . . . . . . . 11
⊢ {∅,
𝐵} ∈
Top |
4 | | eltx 22719 |
. . . . . . . . . . 11
⊢
(({∅, 𝐴}
∈ Top ∧ {∅, 𝐵} ∈ Top) → (𝑥 ∈ ({∅, 𝐴} ×t {∅, 𝐵}) ↔ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
5 | 2, 3, 4 | mp2an 689 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ↔ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) |
6 | | rsp 3131 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
8 | | elssuni 4871 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ⊆ ∪ ({∅, 𝐴} ×t {∅, 𝐵})) |
9 | | indisuni 22153 |
. . . . . . . . . . . . . . 15
⊢ ( I
‘𝐴) = ∪ {∅, 𝐴} |
10 | | indisuni 22153 |
. . . . . . . . . . . . . . 15
⊢ ( I
‘𝐵) = ∪ {∅, 𝐵} |
11 | 2, 3, 9, 10 | txunii 22744 |
. . . . . . . . . . . . . 14
⊢ (( I
‘𝐴) × ( I
‘𝐵)) = ∪ ({∅, 𝐴} ×t {∅, 𝐵}) |
12 | 8, 11 | sseqtrrdi 3972 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ⊆ (( I ‘𝐴) × ( I ‘𝐵))) |
13 | 12 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑥 ⊆ (( I ‘𝐴) × ( I ‘𝐵))) |
14 | | ne0i 4268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑧 × 𝑤) → (𝑧 × 𝑤) ≠ ∅) |
15 | 14 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) ≠ ∅) |
16 | | xpnz 6062 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅) ↔ (𝑧 × 𝑤) ≠ ∅) |
17 | 15, 16 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅)) |
18 | 17 | simpld 495 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ≠ ∅) |
19 | 18 | neneqd 2948 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → ¬ 𝑧 = ∅) |
20 | | simpll 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ∈ {∅, 𝐴}) |
21 | | indislem 22150 |
. . . . . . . . . . . . . . . . . . 19
⊢ {∅,
( I ‘𝐴)} = {∅,
𝐴} |
22 | 20, 21 | eleqtrrdi 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ∈ {∅, ( I ‘𝐴)}) |
23 | | elpri 4583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {∅, ( I
‘𝐴)} → (𝑧 = ∅ ∨ 𝑧 = ( I ‘𝐴))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 = ∅ ∨ 𝑧 = ( I ‘𝐴))) |
25 | 24 | ord 861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (¬ 𝑧 = ∅ → 𝑧 = ( I ‘𝐴))) |
26 | 19, 25 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 = ( I ‘𝐴)) |
27 | 17 | simprd 496 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ≠ ∅) |
28 | 27 | neneqd 2948 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → ¬ 𝑤 = ∅) |
29 | | simplr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ∈ {∅, 𝐵}) |
30 | | indislem 22150 |
. . . . . . . . . . . . . . . . . . 19
⊢ {∅,
( I ‘𝐵)} = {∅,
𝐵} |
31 | 29, 30 | eleqtrrdi 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ∈ {∅, ( I ‘𝐵)}) |
32 | | elpri 4583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {∅, ( I
‘𝐵)} → (𝑤 = ∅ ∨ 𝑤 = ( I ‘𝐵))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑤 = ∅ ∨ 𝑤 = ( I ‘𝐵))) |
34 | 33 | ord 861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (¬ 𝑤 = ∅ → 𝑤 = ( I ‘𝐵))) |
35 | 28, 34 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 = ( I ‘𝐵)) |
36 | 26, 35 | xpeq12d 5620 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) = (( I ‘𝐴) × ( I ‘𝐵))) |
37 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) ⊆ 𝑥) |
38 | 36, 37 | eqsstrrd 3960 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (( I ‘𝐴) × ( I ‘𝐵)) ⊆ 𝑥) |
39 | 38 | adantll 711 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (( I ‘𝐴) × ( I ‘𝐵)) ⊆ 𝑥) |
40 | 13, 39 | eqssd 3938 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵))) |
41 | 40 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) → ((𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
42 | 41 | rexlimdvva 3223 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
43 | 7, 42 | syld 47 |
. . . . . . . 8
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑦 ∈ 𝑥 → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
44 | 43 | exlimdv 1936 |
. . . . . . 7
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (∃𝑦 𝑦 ∈ 𝑥 → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
45 | 1, 44 | syl5bi 241 |
. . . . . 6
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (¬ 𝑥 = ∅ → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
46 | 45 | orrd 860 |
. . . . 5
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑥 = ∅ ∨ 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
47 | | vex 3436 |
. . . . . 6
⊢ 𝑥 ∈ V |
48 | 47 | elpr 4584 |
. . . . 5
⊢ (𝑥 ∈ {∅, (( I
‘𝐴) × ( I
‘𝐵))} ↔ (𝑥 = ∅ ∨ 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
49 | 46, 48 | sylibr 233 |
. . . 4
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ∈ {∅, (( I
‘𝐴) × ( I
‘𝐵))}) |
50 | 49 | ssriv 3925 |
. . 3
⊢
({∅, 𝐴}
×t {∅, 𝐵}) ⊆ {∅, (( I ‘𝐴) × ( I ‘𝐵))} |
51 | 9 | toptopon 22066 |
. . . . . . 7
⊢
({∅, 𝐴} ∈
Top ↔ {∅, 𝐴}
∈ (TopOn‘( I ‘𝐴))) |
52 | 2, 51 | mpbi 229 |
. . . . . 6
⊢ {∅,
𝐴} ∈ (TopOn‘( I
‘𝐴)) |
53 | 10 | toptopon 22066 |
. . . . . . 7
⊢
({∅, 𝐵} ∈
Top ↔ {∅, 𝐵}
∈ (TopOn‘( I ‘𝐵))) |
54 | 3, 53 | mpbi 229 |
. . . . . 6
⊢ {∅,
𝐵} ∈ (TopOn‘( I
‘𝐵)) |
55 | | txtopon 22742 |
. . . . . 6
⊢
(({∅, 𝐴}
∈ (TopOn‘( I ‘𝐴)) ∧ {∅, 𝐵} ∈ (TopOn‘( I ‘𝐵))) → ({∅, 𝐴} ×t {∅,
𝐵}) ∈ (TopOn‘((
I ‘𝐴) × ( I
‘𝐵)))) |
56 | 52, 54, 55 | mp2an 689 |
. . . . 5
⊢
({∅, 𝐴}
×t {∅, 𝐵}) ∈ (TopOn‘(( I ‘𝐴) × ( I ‘𝐵))) |
57 | | topgele 22079 |
. . . . 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 484 |
. . 3
⊢ {∅,
(( I ‘𝐴) × ( I
‘𝐵))} ⊆
({∅, 𝐴}
×t {∅, 𝐵}) |
60 | 50, 59 | eqssi 3937 |
. 2
⊢
({∅, 𝐴}
×t {∅, 𝐵}) = {∅, (( I ‘𝐴) × ( I ‘𝐵))} |
61 | | txindislem 22784 |
. . 3
⊢ (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵)) |
62 | 61 | preq2i 4673 |
. 2
⊢ {∅,
(( I ‘𝐴) × ( I
‘𝐵))} = {∅, ( I
‘(𝐴 × 𝐵))} |
63 | | indislem 22150 |
. 2
⊢ {∅,
( I ‘(𝐴 × 𝐵))} = {∅, (𝐴 × 𝐵)} |
64 | 60, 62, 63 | 3eqtri 2770 |
1
⊢
({∅, 𝐴}
×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)} |