Step |
Hyp |
Ref |
Expression |
1 |
|
ssint |
|- ( A C_ |^| B <-> A. x e. B A C_ x ) |
2 |
|
ssel |
|- ( B C_ On -> ( A e. B -> A e. On ) ) |
3 |
|
ssel |
|- ( B C_ On -> ( x e. B -> x e. On ) ) |
4 |
2 3
|
anim12d |
|- ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A e. On /\ x e. On ) ) ) |
5 |
|
ontri1 |
|- ( ( A e. On /\ x e. On ) -> ( A C_ x <-> -. x e. A ) ) |
6 |
4 5
|
syl6 |
|- ( B C_ On -> ( ( A e. B /\ x e. B ) -> ( A C_ x <-> -. x e. A ) ) ) |
7 |
6
|
expdimp |
|- ( ( B C_ On /\ A e. B ) -> ( x e. B -> ( A C_ x <-> -. x e. A ) ) ) |
8 |
7
|
pm5.74d |
|- ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. B -> -. x e. A ) ) ) |
9 |
|
con2b |
|- ( ( x e. B -> -. x e. A ) <-> ( x e. A -> -. x e. B ) ) |
10 |
8 9
|
bitrdi |
|- ( ( B C_ On /\ A e. B ) -> ( ( x e. B -> A C_ x ) <-> ( x e. A -> -. x e. B ) ) ) |
11 |
10
|
ralbidv2 |
|- ( ( B C_ On /\ A e. B ) -> ( A. x e. B A C_ x <-> A. x e. A -. x e. B ) ) |
12 |
1 11
|
bitrid |
|- ( ( B C_ On /\ A e. B ) -> ( A C_ |^| B <-> A. x e. A -. x e. B ) ) |
13 |
12
|
biimprd |
|- ( ( B C_ On /\ A e. B ) -> ( A. x e. A -. x e. B -> A C_ |^| B ) ) |
14 |
13
|
expimpd |
|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A C_ |^| B ) ) |
15 |
|
intss1 |
|- ( A e. B -> |^| B C_ A ) |
16 |
15
|
a1i |
|- ( B C_ On -> ( A e. B -> |^| B C_ A ) ) |
17 |
16
|
adantrd |
|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> |^| B C_ A ) ) |
18 |
14 17
|
jcad |
|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> ( A C_ |^| B /\ |^| B C_ A ) ) ) |
19 |
|
eqss |
|- ( A = |^| B <-> ( A C_ |^| B /\ |^| B C_ A ) ) |
20 |
18 19
|
syl6ibr |
|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) ) |