Step | Hyp | Ref
| Expression |
1 | | locfincmp.1 |
. . . . . . . . . 10
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | locfinnei 21136 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (LocFin‘𝐽) ∧ 𝑥 ∈ 𝑋) → ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
3 | 2 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝐶 ∈ (LocFin‘𝐽) → ∀𝑥 ∈ 𝑋 ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
4 | 1 | cmpcov2 21003 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) →
∃𝑐 ∈ (𝒫
𝐽 ∩ Fin)(𝑋 = ∪
𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
5 | 3, 4 | sylan2 490 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → ∃𝑐 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
6 | | elfpw 8151 |
. . . . . . . . 9
⊢ (𝑐 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) |
7 | | simplrr 797 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → 𝑐 ∈ Fin) |
8 | | eldifsn 4260 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐶 ∖ {∅}) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅)) |
9 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑥 ∈ 𝐶) |
10 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑦 ∈ 𝑥) |
11 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑦 ∈ 𝑜) |
12 | | inelcm 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ 𝑜) → (𝑥 ∩ 𝑜) ≠ ∅) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → (𝑥 ∩ 𝑜) ≠ ∅) |
14 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑥 → (𝑠 ∩ 𝑜) = (𝑥 ∩ 𝑜)) |
15 | 14 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑥 → ((𝑠 ∩ 𝑜) ≠ ∅ ↔ (𝑥 ∩ 𝑜) ≠ ∅)) |
16 | 15 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ↔ (𝑥 ∈ 𝐶 ∧ (𝑥 ∩ 𝑜) ≠ ∅)) |
17 | 9, 13, 16 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
18 | | elunii 4377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ ∪ 𝐶) |
19 | | locfincmp.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑌 = ∪
𝐶 |
20 | 18, 19 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ 𝑌) |
21 | 20 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑌) |
23 | 1, 19 | locfinbas 21135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐶 ∈ (LocFin‘𝐽) → 𝑋 = 𝑌) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → 𝑋 = 𝑌) |
25 | 24 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑋 = 𝑌) |
26 | 22, 25 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑋) |
27 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑋 = ∪ 𝑐) |
28 | 26, 27 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝑐) |
29 | | eluni2 4376 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ∪ 𝑐
↔ ∃𝑜 ∈
𝑐 𝑦 ∈ 𝑜) |
30 | 28, 29 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → ∃𝑜 ∈ 𝑐 𝑦 ∈ 𝑜) |
31 | 17, 30 | reximddv 3001 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
32 | 31 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (𝑦 ∈ 𝑥 → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
33 | 32 | exlimdv 1848 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
34 | | n0 3890 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
35 | | eliun 4460 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ↔ ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
36 | 33, 34, 35 | 3imtr4g 284 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (𝑥 ≠ ∅ → 𝑥 ∈ ∪
𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
37 | 36 | expimpd 627 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → ((𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅) → 𝑥 ∈ ∪
𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
38 | 8, 37 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (𝑥 ∈ (𝐶 ∖ {∅}) → 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
39 | 38 | ssrdv 3574 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (𝐶 ∖ {∅}) ⊆ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
40 | | iunfi 8137 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ Fin ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) |
41 | 40 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ Fin →
(∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
42 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin ∧ (𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) → (𝐶 ∖ {∅}) ∈
Fin) |
43 | 42 | expcom 450 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} → (∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
44 | 41, 43 | sylan9 687 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ Fin ∧ (𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) → (∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
45 | 7, 39, 44 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
46 | 45 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) → ((𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
47 | 6, 46 | sylan2b 491 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ 𝑐 ∈ (𝒫 𝐽 ∩ Fin)) → ((𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
48 | 47 | rexlimdva 3013 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (∃𝑐 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
49 | 5, 48 | mpd 15 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (𝐶 ∖ {∅}) ∈
Fin) |
50 | | snfi 7923 |
. . . . . 6
⊢ {∅}
∈ Fin |
51 | | unfi 8112 |
. . . . . 6
⊢ (((𝐶 ∖ {∅}) ∈ Fin
∧ {∅} ∈ Fin) → ((𝐶 ∖ {∅}) ∪ {∅}) ∈
Fin) |
52 | 49, 50, 51 | sylancl 693 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → ((𝐶 ∖ {∅}) ∪ {∅}) ∈
Fin) |
53 | | ssun1 3738 |
. . . . . 6
⊢ 𝐶 ⊆ (𝐶 ∪ {∅}) |
54 | | undif1 3995 |
. . . . . 6
⊢ ((𝐶 ∖ {∅}) ∪
{∅}) = (𝐶 ∪
{∅}) |
55 | 53, 54 | sseqtr4i 3601 |
. . . . 5
⊢ 𝐶 ⊆ ((𝐶 ∖ {∅}) ∪
{∅}) |
56 | | ssfi 8065 |
. . . . 5
⊢ ((((𝐶 ∖ {∅}) ∪
{∅}) ∈ Fin ∧ 𝐶 ⊆ ((𝐶 ∖ {∅}) ∪ {∅})) →
𝐶 ∈
Fin) |
57 | 52, 55, 56 | sylancl 693 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → 𝐶 ∈ Fin) |
58 | 57, 24 | jca 553 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (𝐶 ∈ Fin ∧ 𝑋 = 𝑌)) |
59 | 58 | ex 449 |
. 2
⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) → (𝐶 ∈ Fin ∧ 𝑋 = 𝑌))) |
60 | | cmptop 21008 |
. . 3
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
61 | 1, 19 | finlocfin 21133 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽)) |
62 | 61 | 3expib 1260 |
. . 3
⊢ (𝐽 ∈ Top → ((𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽))) |
63 | 60, 62 | syl 17 |
. 2
⊢ (𝐽 ∈ Comp → ((𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽))) |
64 | 59, 63 | impbid 201 |
1
⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) ↔ (𝐶 ∈ Fin ∧ 𝑋 = 𝑌))) |