Step |
Hyp |
Ref |
Expression |
1 |
|
df-sup |
⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } |
2 |
|
dfrab3 |
⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ) |
3 |
|
abeq1 |
⊢ ( { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ∀ 𝑥 ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) ) |
4 |
|
vex |
⊢ 𝑥 ∈ V |
5 |
|
eldif |
⊢ ( 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) |
6 |
4 5
|
mpbiran |
⊢ ( 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
7 |
4
|
elima |
⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝑅 𝑥 ) |
8 |
|
dfrex2 |
⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝑅 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ) |
9 |
7 8
|
bitri |
⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ) |
10 |
4
|
elima |
⊢ ( 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) 𝑦 𝑅 𝑥 ) |
11 |
|
dfrex2 |
⊢ ( ∃ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) 𝑦 𝑅 𝑥 ↔ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) |
12 |
10 11
|
bitri |
⊢ ( 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ↔ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) |
13 |
9 12
|
orbi12i |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ∨ 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ( ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∨ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ) |
14 |
|
elun |
⊢ ( 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ∨ 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
15 |
|
ianor |
⊢ ( ¬ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ( ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∨ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ) |
16 |
13 14 15
|
3bitr4i |
⊢ ( 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ¬ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ) |
17 |
16
|
con2bii |
⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
18 |
|
vex |
⊢ 𝑦 ∈ V |
19 |
18 4
|
brcnv |
⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) |
20 |
19
|
notbii |
⊢ ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 ) |
21 |
20
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ) |
22 |
|
impexp |
⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) ) |
23 |
|
eldif |
⊢ ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ) |
24 |
23
|
imbi1i |
⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ) |
25 |
18
|
elima |
⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑧 ◡ 𝑅 𝑦 ) |
26 |
|
vex |
⊢ 𝑧 ∈ V |
27 |
26 18
|
brcnv |
⊢ ( 𝑧 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑧 ) |
28 |
27
|
rexbii |
⊢ ( ∃ 𝑧 ∈ 𝐵 𝑧 ◡ 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) |
29 |
25 28
|
bitri |
⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) |
30 |
29
|
imbi2i |
⊢ ( ( 𝑦 𝑅 𝑥 → 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) |
31 |
|
con34b |
⊢ ( ( 𝑦 𝑅 𝑥 → 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) |
32 |
30 31
|
bitr3i |
⊢ ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) |
33 |
32
|
imbi2i |
⊢ ( ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) ) |
34 |
22 24 33
|
3bitr4i |
⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
35 |
34
|
ralbii2 |
⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) |
36 |
21 35
|
anbi12i |
⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) |
37 |
6 17 36
|
3bitr2ri |
⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) |
38 |
3 37
|
mpgbir |
⊢ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
39 |
38
|
ineq2i |
⊢ ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ) = ( 𝐴 ∩ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) |
40 |
|
invdif |
⊢ ( 𝐴 ∩ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
41 |
39 40
|
eqtri |
⊢ ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ) = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
42 |
2 41
|
eqtri |
⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
43 |
42
|
unieqi |
⊢ ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |
44 |
1 43
|
eqtri |
⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) |