This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem locfincmp

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses locfincmp.1 ⊢ 𝑋 = ∪ 𝐽
locfincmp.2 ⊢ 𝑌 = ∪ 𝐶
Assertion locfincmp ( 𝐽 ∈ Comp → ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 locfincmp.1 ⊢ 𝑋 = ∪ 𝐽
2 locfincmp.2 ⊢ 𝑌 = ∪ 𝐶
3 1 locfinnei ⊢ ( ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) )
4 3 ralrimiva ⊢ ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) )
5 1 cmpcov2 ⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) ) → ∃ 𝑐 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑐 ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) )
6 4 5 sylan2 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → ∃ 𝑐 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑐 ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) )
7 elfpw ⊢ ( 𝑐 ∈ ( 𝒫 𝐽 ∩ Fin ) ↔ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) )
8 simplrr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) → 𝑐 ∈ Fin )
9 eldifsn ⊢ ( 𝑥 ∈ ( 𝐶 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅ ) )
10 ineq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 ∩ 𝑜 ) = ( 𝑥 ∩ 𝑜 ) )
11 10 neeq1d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑠 ∩ 𝑜 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝑜 ) ≠ ∅ ) )
12 simplrl ⊢ ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜 ) ) → 𝑥 ∈ 𝐶 )
13 simplrr ⊢ ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜 ) ) → 𝑦 ∈ 𝑥 )
14 simprr ⊢ ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜 ) ) → 𝑦 ∈ 𝑜 )
15 inelcm ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ 𝑜 ) → ( 𝑥 ∩ 𝑜 ) ≠ ∅ )
16 13 14 15 syl2anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜 ) ) → ( 𝑥 ∩ 𝑜 ) ≠ ∅ )
17 11 12 16 elrabd ⊢ ( ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜 ) ) → 𝑥 ∈ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } )
18 elunii ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) → 𝑦 ∈ ∪ 𝐶 )
19 18 2 eleqtrrdi ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶 ) → 𝑦 ∈ 𝑌 )
20 19 ancoms ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑌 )
21 20 adantl ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑌 )
22 1 2 locfinbas ⊢ ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) → 𝑋 = 𝑌 )
23 22 adantl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → 𝑋 = 𝑌 )
24 23 ad3antrrr ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑋 = 𝑌 )
25 21 24 eleqtrrd ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑋 )
26 simplr ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑋 = ∪ 𝑐 )
27 25 26 eleqtrd ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ∪ 𝑐 )
28 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝑐 ↔ ∃ 𝑜 ∈ 𝑐 𝑦 ∈ 𝑜 )
29 27 28 sylib ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑜 ∈ 𝑐 𝑦 ∈ 𝑜 )
30 17 29 reximddv ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑜 ∈ 𝑐 𝑥 ∈ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } )
31 30 expr ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 ∈ 𝑥 → ∃ 𝑜 ∈ 𝑐 𝑥 ∈ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) )
32 31 exlimdv ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑥 ∈ 𝐶 ) → ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑜 ∈ 𝑐 𝑥 ∈ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) )
33 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
34 eliun ⊢ ( 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ↔ ∃ 𝑜 ∈ 𝑐 𝑥 ∈ { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } )
35 32 33 34 3imtr4g ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ≠ ∅ → 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) )
36 35 expimpd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) )
37 9 36 biimtrid ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑥 ∈ ( 𝐶 ∖ { ∅ } ) → 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) )
38 37 ssrdv ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) → ( 𝐶 ∖ { ∅ } ) ⊆ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } )
39 iunfi ⊢ ( ( 𝑐 ∈ Fin ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) → ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin )
40 39 ex ⊢ ( 𝑐 ∈ Fin → ( ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin → ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) )
41 ssfi ⊢ ( ( ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ∧ ( 𝐶 ∖ { ∅ } ) ⊆ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) → ( 𝐶 ∖ { ∅ } ) ∈ Fin )
42 41 expcom ⊢ ( ( 𝐶 ∖ { ∅ } ) ⊆ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } → ( ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
43 40 42 sylan9 ⊢ ( ( 𝑐 ∈ Fin ∧ ( 𝐶 ∖ { ∅ } ) ⊆ ∪ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ) → ( ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
44 8 38 43 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) ∧ 𝑋 = ∪ 𝑐 ) → ( ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
45 44 expimpd ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ ( 𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin ) ) → ( ( 𝑋 = ∪ 𝑐 ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
46 7 45 sylan2b ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) ∧ 𝑐 ∈ ( 𝒫 𝐽 ∩ Fin ) ) → ( ( 𝑋 = ∪ 𝑐 ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
47 46 rexlimdva ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → ( ∃ 𝑐 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑐 ∧ ∀ 𝑜 ∈ 𝑐 { 𝑠 ∈ 𝐶 ∣ ( 𝑠 ∩ 𝑜 ) ≠ ∅ } ∈ Fin ) → ( 𝐶 ∖ { ∅ } ) ∈ Fin ) )
48 6 47 mpd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → ( 𝐶 ∖ { ∅ } ) ∈ Fin )
49 snfi ⊢ { ∅ } ∈ Fin
50 unfi ⊢ ( ( ( 𝐶 ∖ { ∅ } ) ∈ Fin ∧ { ∅ } ∈ Fin ) → ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin )
51 48 49 50 sylancl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin )
52 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ { ∅ } )
53 undif1 ⊢ ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } ) = ( 𝐶 ∪ { ∅ } )
54 52 53 sseqtrri ⊢ 𝐶 ⊆ ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } )
55 ssfi ⊢ ( ( ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin ∧ 𝐶 ⊆ ( ( 𝐶 ∖ { ∅ } ) ∪ { ∅ } ) ) → 𝐶 ∈ Fin )
56 51 54 55 sylancl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → 𝐶 ∈ Fin )
57 56 23 jca ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) → ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) )
58 57 ex ⊢ ( 𝐽 ∈ Comp → ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) → ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) ) )
59 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
60 1 2 finlocfin ⊢ ( ( 𝐽 ∈ Top ∧ 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐶 ∈ ( LocFin ‘ 𝐽 ) )
61 60 3expib ⊢ ( 𝐽 ∈ Top → ( ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) )
62 59 61 syl ⊢ ( 𝐽 ∈ Comp → ( ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) → 𝐶 ∈ ( LocFin ‘ 𝐽 ) ) )
63 58 62 impbid ⊢ ( 𝐽 ∈ Comp → ( 𝐶 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐶 ∈ Fin ∧ 𝑋 = 𝑌 ) ) )