Step |
Hyp |
Ref |
Expression |
1 |
|
soss |
⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → 𝑅 Or 𝐵 ) ) |
2 |
|
simp1 |
⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → 𝑅 Or 𝐵 ) |
3 |
|
fisupg |
⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
4 |
2 3
|
supeu |
⊢ ( ( 𝑅 Or 𝐵 ∧ 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ) → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
5 |
4
|
3exp |
⊢ ( 𝑅 Or 𝐵 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) ) |
6 |
1 5
|
syl6 |
⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Or 𝐴 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) ) ) |
7 |
6
|
com4l |
⊢ ( 𝑅 Or 𝐴 → ( 𝐵 ∈ Fin → ( 𝐵 ≠ ∅ → ( 𝐵 ⊆ 𝐴 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) ) ) |
8 |
7
|
3imp2 |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
9 |
|
reurex |
⊢ ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
10 |
|
breq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝑥 ) ) |
11 |
10
|
rspcev |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) |
12 |
11
|
ex |
⊢ ( 𝑥 ∈ 𝐵 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) |
13 |
12
|
ralrimivw |
⊢ ( 𝑥 ∈ 𝐵 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) |
14 |
13
|
a1d |
⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
15 |
14
|
anim2d |
⊢ ( 𝑥 ∈ 𝐵 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) |
16 |
15
|
reximia |
⊢ ( ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
17 |
8 9 16
|
3syl |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |