Step |
Hyp |
Ref |
Expression |
1 |
|
supmo.1 |
⊢ ( 𝜑 → 𝑅 Or 𝐴 ) |
2 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑅 Or 𝐴 ) |
3 |
2
|
supval2 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) |
4 |
|
3simpc |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
6 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝐶 ∈ 𝐴 ) |
7 |
|
breq1 |
⊢ ( 𝑥 = 𝐶 → ( 𝑥 𝑅 𝑦 ↔ 𝐶 𝑅 𝑦 ) ) |
8 |
7
|
notbid |
⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝐶 𝑅 𝑦 ) ) |
9 |
8
|
ralbidv |
⊢ ( 𝑥 = 𝐶 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ) ) |
10 |
|
breq2 |
⊢ ( 𝑥 = 𝐶 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐶 ) ) |
11 |
10
|
imbi1d |
⊢ ( 𝑥 = 𝐶 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑥 = 𝐶 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
13 |
9 12
|
anbi12d |
⊢ ( 𝑥 = 𝐶 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ) |
14 |
13
|
rspcev |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
15 |
6 5 14
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
16 |
2 15
|
supeu |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
17 |
13
|
riota2 |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 ) ) |
18 |
6 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 ) ) |
19 |
5 18
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 ) |
20 |
3 19
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) |
21 |
20
|
ex |
⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) ) |