transversal of set of sets statements equivalence proof

Question

Let A be a set of sets and Y is a transversal for A. Prove that the following two statements are equivalent:

(i) $(\forall y \in Y)(\exists X \in A)((Y \setminus \{y\}) \cap X = \emptyset)$

(ii) $(\forall y \in Y)(\exists X \in A)((Y \cap X = \{y\}))$

Where transversal for a set of sets A is a set for which, every time when $X \in A$, it is true that $X \cap Y \neq \emptyset$

I know how to prove that the following two are equivalent:

(iii) Y is a minimal transversal of A

(iv) $(\forall y \in Y)(\exists X \in A)((Y \cap X = \{y\}))$,

where minimal transversal has the following definition:

Let Y be a transversal for A. We say that Y is minimal transversal for A, if every time when $Y' \subsetneqq Y \implies Y' $ is not a transversal.

My question is: How do I move from the first two statements which I'm not so sure how to prove, to the last two statements which I know how to prove? More precisely, (ii) and (iv) are equivalent, so can I derive (iii) from (i) and use the proof that I know, i.e. how do I prove (i) is equivalent to (iii)?

Note: I need to do this in the most rigorous and formal way as possible.

Thanks in advance!

Answer 1

No need to bother with minimal tranversals ... just use the fact that $Y$ is a transversal for $A$

To go from (i) to (ii):

Take any $y \in Y$. From (i) this means that there is some $X \in A$ such that $(Y \setminus \{y\}) \cap X = \emptyset$

Since $Y$ is a transversal for $A$, it must be the case that $X \cap Y \not = \emptyset$, and the only way for $(Y \setminus \{y\}) \cap X = \emptyset$ and $X \cap Y \not = \emptyset$ to be both true is for $y \in X$, for if $y \not \in X$, then $(Y \setminus \{y\}) \cap X = X \cap Y$. Hence $(X \cap Y = X \cap (Y \setminus \{y\}) \cup (X \cap \{ y \}) = \emptyset \cup \{ y \} = \{ y \}$

From (ii) to (i):

Take any $y \in Y$. From (ii) this means that there is some $X \in A$ such that $Y \cap X = \{ y \}$, i.e. $X$ and $Y$ have only $y$ as a common element. But then it immediately follows that $(Y \setminus \{y\}) \cap X = \emptyset$

I need to do this in the most rigorous and formal way as possible.

OK:

1. ∀x ∀y (y = transversal(x) ↔ ∀z (z ∈ x → ¬int(y,z) = e)) (definition transversal)
2. ∀x ∀y ∀z (z ∈ int(x,y) ↔ (z ∈ x ∧ z ∈ y)) (definition intersection)
3. ∀x ∀y (x = y ↔ ∀z (z ∈ x ↔ z ∈ y)) (definition set identity)
4. ∀x ¬x ∈ e (definition empty set)
5. ∀x ∀y ∀z (z ∈ setminus(x,y) ↔ (z ∈ x ∧ ¬z ∈ y)) (definition setminus)
6. ∀x ∀y (y ∈ singleton(x) ↔ y = x) (definition singleton)
7. (introduce a,b) b = transversal(a) (Assumption)
8. b = transversal(a) ↔ ∀z (z ∈ a → ¬int(b,z) = e) ∀ Elim : 1
9. ∀z (z ∈ a → ¬int(b,z) = e) ↔ Elim : 7, 8
10. ∀w (w ∈ b → ∃z (z ∈ a ∧ int(setminus(b,singleton(w)),z) = e)) (Assumption)
11. (introduce c) c ∈ b (Assumption)
12. c ∈ b → ∃z (z ∈ a ∧ int(setminus(b,singleton(c)),z) = e) ∀ Elim : 10
13. ∃z (z ∈ a ∧ int(setminus(b,singleton(c)),z) = e) → Elim : 11, 12
14. (introduce d) d ∈ a ∧ int(setminus(b,singleton(c)),d) = e (Assumption)
15. d ∈ a ∧ Elim : 14
16. int(setminus(b,singleton(c)),d) = e ∧ Elim : 14
17. d ∈ a → ¬int(b,d) = e ∀ Elim : 9
18. ¬int(b,d) = e → Elim : 15, 17
19. (introduce f) f ∈ int(d,b) (Assumption)
20. f ∈ int(d,b) ↔ (f ∈ d ∧ f ∈ b) ∀ Elim : 2
21. f ∈ d ∧ f ∈ b ↔ Elim : 19, 20
22. f ∈ d ∧ Elim : 21
23. f ∈ b ∧ Elim : 21
24. ¬f = c (Assumption)
25. f ∈ singleton(c) (Assumption)
26. f ∈ singleton(c) ↔ f = c ∀ Elim : 6
27. f = c ↔ Elim : 25, 26
28. ⊥ ⊥ Intro : 27, 24
29. ¬f ∈ singleton(c) ¬ Intro : 25-28
30. f ∈ b ∧ ¬f ∈ singleton(c) ∧ Intro : 23, 29
31. f ∈ setminus(b,singleton(c)) ↔ (f ∈ b ∧ ¬f ∈ singleton(c)) ∀ Elim : 5
32. f ∈ setminus(b,singleton(c)) ↔ Elim : 31, 30
33. f ∈ setminus(b,singleton(c)) ∧ f ∈ d ∧ Intro : 22, 32
34. f ∈ int(setminus(b,singleton(c)),d) ↔ (f ∈ setminus(b,singleton(c)) ∧ f ∈ d) ∀ Elim : 2
35. f ∈ int(setminus(b,singleton(c)),d) ↔ Elim : 33, 34
36. f ∈ e = Elim : 16, 35
37. ¬f ∈ e ∀ Elim : 4
38. ⊥ ⊥ Intro : 36, 37
39. f = c ¬ Intro : 24-38
40. ∀v (v ∈ int(d,b) → v = c) ∀ Intro : 19-39
41. (introduce f)
42. f ∈ int(d,b) (Assumption)
43. f ∈ int(d,b) → f = c ∀ Elim : 40
44. f = c → Elim : 42, 43
45. f = c (Assumption)
46. f ∈ singleton(c) ↔ f = c ∀ Elim : 6
47. f ∈ singleton(c) ↔ Elim : 45, 46
48. f ∈ b = Elim : 45, 11
49. ¬f ∈ d (Assumption)
50. (introduce c0)
51. c0 ∈ int(setminus(b,singleton(c)),d) ↔ (c0 ∈ setminus(b,singleton(c)) ∧ c0 ∈ d) ∀ Elim : 2
52. c0 ∈ int(b,d) ↔ (c0 ∈ b ∧ c0 ∈ d) ∀ Elim : 2
53. c0 ∈ setminus(b,singleton(c)) ↔ (c0 ∈ b ∧ ¬c0 ∈ singleton(c)) ∀ Elim : 5
54. c0 ∈ int(b,d) (Assumption)
55. c0 ∈ b ∧ c0 ∈ d ↔ Elim : 54, 52
56. c0 ∈ b ∧ Elim : 55
57. c0 ∈ d ∧ Elim : 55
58. c0 ∈ singleton(c) (Assumption)
59. c0 ∈ singleton(c) ↔ c0 = c ∀ Elim : 6
60. c0 = c ↔ Elim : 58, 59
61. c ∈ d = Elim : 60, 57
62. f ∈ d = Elim : 45, 61
63. ⊥ ⊥ Intro : 62, 49
64. ¬c0 ∈ singleton(c) ¬ Intro : 58-63
65. c0 ∈ b ∧ ¬c0 ∈ singleton(c) ∧ Intro : 64, 56
66. c0 ∈ setminus(b,singleton(c)) ↔ Elim : 65, 53
67. c0 ∈ setminus(b,singleton(c)) ∧ c0 ∈ d ∧ Intro : 66, 57
68. c0 ∈ int(setminus(b,singleton(c)),d) ↔ Elim : 67, 51
69. c0 ∈ int(setminus(b,singleton(c)),d) (Assumption)
70. c0 ∈ setminus(b,singleton(c)) ∧ c0 ∈ d ↔ Elim : 69, 51
71. c0 ∈ setminus(b,singleton(c)) ∧ Elim : 70
72. c0 ∈ d ∧ Elim : 70
73. c0 ∈ b ∧ ¬c0 ∈ singleton(c) ↔ Elim : 71, 53
74. c0 ∈ b ∧ Elim : 73
75. c0 ∈ b ∧ c0 ∈ d ∧ Intro : 72, 74
76. c0 ∈ int(b,d) ↔ Elim : 75, 52
77. c0 ∈ int(b,d) ↔ c0 ∈ int(setminus(b,singleton(c)),d) ↔ Intro : 54-68, 69-76
78. ∀z (z ∈ int(b,d) ↔ z ∈ int(setminus(b,singleton(c)),d)) ∀ Intro : 50-77
79. int(b,d) = int(setminus(b,singleton(c)),d) ↔ ∀z (z ∈ int(b,d) ↔ z ∈ int(setminus(b,singleton(c)),d)) ∀ Elim : 3
80. int(b,d) = int(setminus(b,singleton(c)),d) ↔ Elim : 78, 79
81. int(b,d) = e = Elim : 16, 80
82. ⊥ ⊥ Intro : 81, 18
83. f ∈ d ¬ Intro : 49-82
84. f ∈ d ∧ f ∈ b ∧ Intro : 83, 48
85. f ∈ int(d,b) ↔ (f ∈ d ∧ f ∈ b) ∀ Elim : 2
86. f ∈ int(d,b) ↔ Elim : 84, 85
87. f ∈ int(d,b) ↔ f = c ↔ Intro : 42-44, 45-86
88. ∀v (v ∈ int(d,b) ↔ v = c) ∀ Intro : 41-87
89. d ∈ a ∧ ∀v (v ∈ int(d,b) ↔ v = c) ∧ Intro : 15, 88
90. ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = c)) ∃ Intro : 89
91. ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = c)) ∃ Elim : 13, 14-90
92. ∀w (w ∈ b → ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = w))) ∀ Intro : 11-91
93. ∀w (w ∈ b → ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = w)))
94. (introduce c) c ∈ b (Assumption)
95. c ∈ b → ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = c)) ∀ Elim : 93
96. ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = c)) → Elim : 94, 95
97. (introduce d) d ∈ a ∧ ∀v (v ∈ int(d,b) ↔ v = c)
98. d ∈ a ∧ Elim : 97
99. ∀v (v ∈ int(d,b) ↔ v = c) ∧ Elim : 97
100. (introduce f)
101. f ∈ int(setminus(b,singleton(c)),d) (Assumption)
102. f ∈ int(setminus(b,singleton(c)),d) ↔ (f ∈ setminus(b,singleton(c)) ∧ f ∈ d) ∀ Elim : 2
103. f ∈ setminus(b,singleton(c)) ∧ f ∈ d ↔ Elim : 101, 102
104. f ∈ setminus(b,singleton(c)) ∧ Elim : 103
105. f ∈ d ∧ Elim : 103
106. f ∈ setminus(b,singleton(c)) ↔ (f ∈ b ∧ ¬f ∈ singleton(c)) ∀ Elim : 5
107. f ∈ b ∧ ¬f ∈ singleton(c) ↔ Elim : 104, 106
108. f ∈ b ∧ Elim : 107
109. ¬f ∈ singleton(c) ∧ Elim : 107
110. f ∈ d ∧ f ∈ b ∧ Intro : 105, 108
111. f ∈ int(d,b) ↔ (f ∈ d ∧ f ∈ b) ∀ Elim : 2
112. f ∈ int(d,b) ↔ Elim : 110, 111
113. f ∈ int(d,b) ↔ f = c ∀ Elim : 99
114. f = c ↔ Elim : 112, 113
115. f ∈ singleton(c) ↔ f = c ∀ Elim : 6
116. f ∈ singleton(c) ↔ Elim : 115, 114
117. ⊥ ⊥ Intro : 116, 109
118. f ∈ e ⊥ Elim : 117
119. f ∈ e
120. ¬f ∈ e ∀ Elim : 4
121. ⊥ ⊥ Intro : 119, 120
122. f ∈ int(setminus(b,singleton(c)),d) ⊥ Elim : 121
123. f ∈ int(setminus(b,singleton(c)),d) ↔ f ∈ e ↔ Intro : 101-118, 119-122
124. ∀z (z ∈ int(setminus(b,singleton(c)),d) ↔ z ∈ e) ∀ Intro : 100-123
125. int(setminus(b,singleton(c)),d) = e ↔ ∀z (z ∈ int(setminus(b,singleton(c)),d) ↔ z ∈ e) ∀ Elim : 3
126. int(setminus(b,singleton(c)),d) = e ↔ Elim : 124, 125
127. d ∈ a ∧ int(setminus(b,singleton(c)),d) = e ∧ Intro : 98, 126
128. ∃z (z ∈ a ∧ int(setminus(b,singleton(c)),z) = e) ∃ Intro : 127
129. ∃z (z ∈ a ∧ int(setminus(b,singleton(c)),z) = e) ∃ Elim : 96, 97-128
130. ∀w (w ∈ b → ∃z (z ∈ a ∧ int(setminus(b,singleton(w)),z) = e)) ∀ Intro : 94-129
131. ∀w (w ∈ b → ∃z (z ∈ a ∧ int(setminus(b,singleton(w)),z) = e)) ↔ ∀w (w ∈ b → ∃z (z ∈ a ∧ ∀v (v ∈ int(z,b) ↔ v = w))) ↔ Intro : 10-92, 93-130
132. ∀x ∀y (y = transversal(x) → (∀w (w ∈ y → ∃z (z ∈ x ∧ int(setminus(y,singleton(w)),z) = e)) ↔ ∀w (w ∈ y → ∃z (z ∈ x ∧ ∀v (v ∈ int(z,y) ↔ v = w))))) ∀ Intro : 7-131

Answer 2

For the equivalence of (i) and (ii): For any $X,Y,y$ we have $[(Y$ \ $\{y\})\cap X]\cup \{y\}=$ $(Y\cap X)\cup \{y\} $ and also we have $(Y$ \ $\{y\}) \cap X=(Y\cap X)$ \ $\{y\}.$

So if $Y\cap X \ne \phi$ then

$\bullet \quad(Y$ \ $\{y\})\cap X=\phi \implies$

$\implies [(Y$ \ $\{y\})\cap X]\cup \{y\}=\phi \cup \{y\}=\{y\} \implies $

$\implies [(Y \cap X)\cup \{y\}]=\{y\} \implies$

$ \implies \phi \ne Y\cap X\subset \{y\}\implies$

$\bullet\quad \implies Y\cap X=\{y\}\implies$

$\bullet \quad \implies (Y$ \ $\{y\}) \cap X=(Y\cap X)$ \ $\{y\}=\{y\}$ \ $\{y\}=\phi.$