| Step |
Hyp |
Ref |
Expression |
| 1 |
|
haustop |
⊢ ( 𝑥 ∈ Haus → 𝑥 ∈ Top ) |
| 2 |
1
|
ssriv |
⊢ Haus ⊆ Top |
| 3 |
|
fss |
⊢ ( ( 𝐹 : 𝐴 ⟶ Haus ∧ Haus ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top ) |
| 4 |
2 3
|
mpan2 |
⊢ ( 𝐹 : 𝐴 ⟶ Haus → 𝐹 : 𝐴 ⟶ Top ) |
| 5 |
|
pttop |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∏t ‘ 𝐹 ) ∈ Top ) |
| 6 |
4 5
|
sylan2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ( ∏t ‘ 𝐹 ) ∈ Top ) |
| 7 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 8 |
|
eqid |
⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 ) |
| 9 |
8
|
ptuni |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 10 |
4 9
|
sylan2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 11 |
10
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 12 |
7 11
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 13 |
|
ixpfn |
⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → 𝑥 Fn 𝐴 ) |
| 14 |
12 13
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 Fn 𝐴 ) |
| 15 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 16 |
15 11
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 17 |
|
ixpfn |
⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → 𝑦 Fn 𝐴 ) |
| 18 |
16 17
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 Fn 𝐴 ) |
| 19 |
|
eqfnfv |
⊢ ( ( 𝑥 Fn 𝐴 ∧ 𝑦 Fn 𝐴 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) ) |
| 20 |
14 18 19
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) ) |
| 21 |
20
|
necon3abid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 ≠ 𝑦 ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) ) |
| 22 |
|
rexnal |
⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) |
| 23 |
|
df-ne |
⊢ ( ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ↔ ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) |
| 24 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → 𝐹 : 𝐴 ⟶ Haus ) |
| 25 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → 𝑘 ∈ 𝐴 ) |
| 26 |
24 25
|
ffvelcdmd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ Haus ) |
| 27 |
|
vex |
⊢ 𝑥 ∈ V |
| 28 |
27
|
elixp |
⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑥 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
| 29 |
28
|
simprbi |
⊢ ( 𝑥 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 30 |
12 29
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 31 |
30
|
r19.21bi |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 32 |
31
|
adantrr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 33 |
|
vex |
⊢ 𝑦 ∈ V |
| 34 |
33
|
elixp |
⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑦 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
| 35 |
34
|
simprbi |
⊢ ( 𝑦 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 36 |
16 35
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 37 |
36
|
r19.21bi |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 38 |
37
|
adantrr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) |
| 39 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) |
| 40 |
|
eqid |
⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) |
| 41 |
40
|
hausnei |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Haus ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑦 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
| 42 |
26 32 38 39 41
|
syl13anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) |
| 43 |
|
simp-4l |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐴 ∈ 𝑉 ) |
| 44 |
4
|
ad4antlr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝐹 : 𝐴 ⟶ Top ) |
| 45 |
25
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑘 ∈ 𝐴 ) |
| 46 |
|
eqid |
⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 ) |
| 47 |
46 8
|
ptpjcn |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ) |
| 48 |
43 44 45 47
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ) |
| 49 |
|
simprll |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ) |
| 50 |
|
eqid |
⊢ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) = ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) |
| 51 |
50
|
mptpreima |
⊢ ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑚 ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } |
| 52 |
|
cnima |
⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑚 ) ∈ ( ∏t ‘ 𝐹 ) ) |
| 53 |
51 52
|
eqeltrrid |
⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) ) |
| 54 |
48 49 53
|
syl2anc |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) ) |
| 55 |
|
simprlr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) |
| 56 |
50
|
mptpreima |
⊢ ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑛 ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } |
| 57 |
|
cnima |
⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ◡ ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) “ 𝑛 ) ∈ ( ∏t ‘ 𝐹 ) ) |
| 58 |
56 57
|
eqeltrrid |
⊢ ( ( ( 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ↦ ( 𝑧 ‘ 𝑘 ) ) ∈ ( ( ∏t ‘ 𝐹 ) Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) ) |
| 59 |
48 55 58
|
syl2anc |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) ) |
| 60 |
|
fveq1 |
⊢ ( 𝑧 = 𝑥 → ( 𝑧 ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) ) |
| 61 |
60
|
eleq1d |
⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ↔ ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ) ) |
| 62 |
7
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 63 |
|
simprr1 |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ) |
| 64 |
61 62 63
|
elrabd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ) |
| 65 |
|
fveq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) ) |
| 66 |
65
|
eleq1d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ↔ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ) ) |
| 67 |
15
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 68 |
|
simprr2 |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ) |
| 69 |
66 67 68
|
elrabd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) |
| 70 |
|
inrab |
⊢ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) } |
| 71 |
|
simprr3 |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( 𝑚 ∩ 𝑛 ) = ∅ ) |
| 72 |
|
inelcm |
⊢ ( ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) → ( 𝑚 ∩ 𝑛 ) ≠ ∅ ) |
| 73 |
72
|
necon2bi |
⊢ ( ( 𝑚 ∩ 𝑛 ) = ∅ → ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) ) |
| 74 |
71 73
|
syl |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) ) |
| 75 |
74
|
ralrimivw |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ∀ 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) ) |
| 76 |
|
rabeq0 |
⊢ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) } = ∅ ↔ ∀ 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ¬ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) ) |
| 77 |
75 76
|
sylibr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 ) } = ∅ ) |
| 78 |
70 77
|
eqtrid |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) |
| 79 |
|
eleq2 |
⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ) ) |
| 80 |
|
ineq1 |
⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( 𝑢 ∩ 𝑣 ) = ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) ) |
| 81 |
80
|
eqeq1d |
⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) ) |
| 82 |
79 81
|
3anbi13d |
⊢ ( 𝑢 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) ) ) |
| 83 |
|
eleq2 |
⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) ) |
| 84 |
|
ineq2 |
⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) ) |
| 85 |
84
|
eqeq1d |
⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ↔ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) ) |
| 86 |
83 85
|
3anbi23d |
⊢ ( 𝑣 = { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } → ( ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ 𝑣 ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ 𝑣 ) = ∅ ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) ) ) |
| 87 |
82 86
|
rspc2ev |
⊢ ( ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∈ ( ∏t ‘ 𝐹 ) ∧ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∈ ( ∏t ‘ 𝐹 ) ∧ ( 𝑥 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∧ 𝑦 ∈ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ∧ ( { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑚 } ∩ { 𝑧 ∈ ∪ ( ∏t ‘ 𝐹 ) ∣ ( 𝑧 ‘ 𝑘 ) ∈ 𝑛 } ) = ∅ ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
| 88 |
54 59 64 69 78 87
|
syl113anc |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
| 89 |
88
|
expr |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) ∧ ( 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 90 |
89
|
rexlimdvva |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ( ∃ 𝑚 ∈ ( 𝐹 ‘ 𝑘 ) ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑘 ) ( ( 𝑥 ‘ 𝑘 ) ∈ 𝑚 ∧ ( 𝑦 ‘ 𝑘 ) ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 91 |
42 90
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) ) ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) |
| 92 |
91
|
expr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑥 ‘ 𝑘 ) ≠ ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 93 |
23 92
|
biimtrrid |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 94 |
93
|
rexlimdva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 95 |
22 94
|
biimtrrid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑘 ) → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 96 |
21 95
|
sylbid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 97 |
96
|
ralrimivva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) |
| 98 |
46
|
ishaus |
⊢ ( ( ∏t ‘ 𝐹 ) ∈ Haus ↔ ( ( ∏t ‘ 𝐹 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ∏t ‘ 𝐹 ) ∃ 𝑣 ∈ ( ∏t ‘ 𝐹 ) ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) ) |
| 99 |
6 97 98
|
sylanbrc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Haus ) → ( ∏t ‘ 𝐹 ) ∈ Haus ) |