Step | Hyp | Ref
| Expression |
1 | | neq0 4234 |
. . . . . . 7
⊢ (¬
𝑥 = ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
2 | | indistop 21753 |
. . . . . . . . . . 11
⊢ {∅,
𝐴} ∈
Top |
3 | | indistop 21753 |
. . . . . . . . . . 11
⊢ {∅,
𝐵} ∈
Top |
4 | | eltx 22319 |
. . . . . . . . . . 11
⊢
(({∅, 𝐴}
∈ Top ∧ {∅, 𝐵} ∈ Top) → (𝑥 ∈ ({∅, 𝐴} ×t {∅, 𝐵}) ↔ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
5 | 2, 3, 4 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ↔ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) |
6 | | rsp 3118 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑥 ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
7 | 5, 6 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥))) |
8 | | elssuni 4828 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ⊆ ∪ ({∅, 𝐴} ×t {∅, 𝐵})) |
9 | | indisuni 21754 |
. . . . . . . . . . . . . . 15
⊢ ( I
‘𝐴) = ∪ {∅, 𝐴} |
10 | | indisuni 21754 |
. . . . . . . . . . . . . . 15
⊢ ( I
‘𝐵) = ∪ {∅, 𝐵} |
11 | 2, 3, 9, 10 | txunii 22344 |
. . . . . . . . . . . . . 14
⊢ (( I
‘𝐴) × ( I
‘𝐵)) = ∪ ({∅, 𝐴} ×t {∅, 𝐵}) |
12 | 8, 11 | sseqtrrdi 3928 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ⊆ (( I ‘𝐴) × ( I ‘𝐵))) |
13 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑥 ⊆ (( I ‘𝐴) × ( I ‘𝐵))) |
14 | | ne0i 4223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑧 × 𝑤) → (𝑧 × 𝑤) ≠ ∅) |
15 | 14 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) ≠ ∅) |
16 | | xpnz 5991 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅) ↔ (𝑧 × 𝑤) ≠ ∅) |
17 | 15, 16 | sylibr 237 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 ≠ ∅ ∧ 𝑤 ≠ ∅)) |
18 | 17 | simpld 498 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ≠ ∅) |
19 | 18 | neneqd 2939 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → ¬ 𝑧 = ∅) |
20 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ∈ {∅, 𝐴}) |
21 | | indislem 21751 |
. . . . . . . . . . . . . . . . . . 19
⊢ {∅,
( I ‘𝐴)} = {∅,
𝐴} |
22 | 20, 21 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑧 ∈ {∅, ( I ‘𝐴)}) |
23 | | elpri 4538 |
. . . . . . . . . . . . . . . . . 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 499 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ≠ ∅) |
28 | 27 | neneqd 2939 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → ¬ 𝑤 = ∅) |
29 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ∈ {∅, 𝐵}) |
30 | | indislem 21751 |
. . . . . . . . . . . . . . . . . . 19
⊢ {∅,
( I ‘𝐵)} = {∅,
𝐵} |
31 | 29, 30 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑤 ∈ {∅, ( I ‘𝐵)}) |
32 | | elpri 4538 |
. . . . . . . . . . . . . . . . . 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 5556 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) = (( I ‘𝐴) × ( I ‘𝐵))) |
37 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (𝑧 × 𝑤) ⊆ 𝑥) |
38 | 36, 37 | eqsstrrd 3916 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵}) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (( I ‘𝐴) × ( I ‘𝐵)) ⊆ 𝑥) |
39 | 38 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → (( I ‘𝐴) × ( I ‘𝐵)) ⊆ 𝑥) |
40 | 13, 39 | eqssd 3894 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) ∧ (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥)) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵))) |
41 | 40 | ex 416 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) ∧ (𝑧 ∈ {∅, 𝐴} ∧ 𝑤 ∈ {∅, 𝐵})) → ((𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
42 | 41 | rexlimdvva 3204 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (∃𝑧 ∈ {∅, 𝐴}∃𝑤 ∈ {∅, 𝐵} (𝑦 ∈ (𝑧 × 𝑤) ∧ (𝑧 × 𝑤) ⊆ 𝑥) → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
43 | 7, 42 | syld 47 |
. . . . . . . 8
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑦 ∈ 𝑥 → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
44 | 43 | exlimdv 1940 |
. . . . . . 7
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (∃𝑦 𝑦 ∈ 𝑥 → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
45 | 1, 44 | syl5bi 245 |
. . . . . 6
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (¬ 𝑥 = ∅ → 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
46 | 45 | orrd 862 |
. . . . 5
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → (𝑥 = ∅ ∨ 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
47 | | vex 3402 |
. . . . . 6
⊢ 𝑥 ∈ V |
48 | 47 | elpr 4539 |
. . . . 5
⊢ (𝑥 ∈ {∅, (( I
‘𝐴) × ( I
‘𝐵))} ↔ (𝑥 = ∅ ∨ 𝑥 = (( I ‘𝐴) × ( I ‘𝐵)))) |
49 | 46, 48 | sylibr 237 |
. . . 4
⊢ (𝑥 ∈ ({∅, 𝐴} ×t {∅,
𝐵}) → 𝑥 ∈ {∅, (( I
‘𝐴) × ( I
‘𝐵))}) |
50 | 49 | ssriv 3881 |
. . 3
⊢
({∅, 𝐴}
×t {∅, 𝐵}) ⊆ {∅, (( I ‘𝐴) × ( I ‘𝐵))} |
51 | 9 | toptopon 21668 |
. . . . . . 7
⊢
({∅, 𝐴} ∈
Top ↔ {∅, 𝐴}
∈ (TopOn‘( I ‘𝐴))) |
52 | 2, 51 | mpbi 233 |
. . . . . 6
⊢ {∅,
𝐴} ∈ (TopOn‘( I
‘𝐴)) |
53 | 10 | toptopon 21668 |
. . . . . . 7
⊢
({∅, 𝐵} ∈
Top ↔ {∅, 𝐵}
∈ (TopOn‘( I ‘𝐵))) |
54 | 3, 53 | mpbi 233 |
. . . . . 6
⊢ {∅,
𝐵} ∈ (TopOn‘( I
‘𝐵)) |
55 | | txtopon 22342 |
. . . . . 6
⊢
(({∅, 𝐴}
∈ (TopOn‘( I ‘𝐴)) ∧ {∅, 𝐵} ∈ (TopOn‘( I ‘𝐵))) → ({∅, 𝐴} ×t {∅,
𝐵}) ∈ (TopOn‘((
I ‘𝐴) × ( I
‘𝐵)))) |
56 | 52, 54, 55 | mp2an 692 |
. . . . 5
⊢
({∅, 𝐴}
×t {∅, 𝐵}) ∈ (TopOn‘(( I ‘𝐴) × ( I ‘𝐵))) |
57 | | topgele 21681 |
. . . . 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 487 |
. . 3
⊢ {∅,
(( I ‘𝐴) × ( I
‘𝐵))} ⊆
({∅, 𝐴}
×t {∅, 𝐵}) |
60 | 50, 59 | eqssi 3893 |
. 2
⊢
({∅, 𝐴}
×t {∅, 𝐵}) = {∅, (( I ‘𝐴) × ( I ‘𝐵))} |
61 | | txindislem 22384 |
. . 3
⊢ (( I
‘𝐴) × ( I
‘𝐵)) = ( I
‘(𝐴 × 𝐵)) |
62 | 61 | preq2i 4628 |
. 2
⊢ {∅,
(( I ‘𝐴) × ( I
‘𝐵))} = {∅, ( I
‘(𝐴 × 𝐵))} |
63 | | indislem 21751 |
. 2
⊢ {∅,
( I ‘(𝐴 × 𝐵))} = {∅, (𝐴 × 𝐵)} |
64 | 60, 62, 63 | 3eqtri 2765 |
1
⊢
({∅, 𝐴}
×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)} |