Step |
Hyp |
Ref |
Expression |
1 |
|
ssref.1 |
⊢ 𝑋 = ∪ 𝐴 |
2 |
|
ssref.2 |
⊢ 𝑌 = ∪ 𝐵 |
3 |
|
eqcom |
⊢ ( 𝑋 = 𝑌 ↔ 𝑌 = 𝑋 ) |
4 |
3
|
biimpi |
⊢ ( 𝑋 = 𝑌 → 𝑌 = 𝑋 ) |
5 |
4
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝑌 = 𝑋 ) |
6 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 ) |
7 |
6
|
3ad2antl2 |
⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 ) |
8 |
|
ssid |
⊢ 𝑥 ⊆ 𝑥 |
9 |
|
sseq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑥 ) ) |
10 |
9
|
rspcev |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) |
11 |
7 8 10
|
sylancl |
⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) |
12 |
11
|
ralrimiva |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) |
13 |
1 2
|
isref |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) ) |
14 |
13
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) ) |
15 |
5 12 14
|
mpbir2and |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 Ref 𝐵 ) |