Step |
Hyp |
Ref |
Expression |
1 |
|
ordelon |
|- ( ( Ord A /\ B e. A ) -> B e. On ) |
2 |
|
onelss |
|- ( B e. On -> ( x e. B -> x C_ B ) ) |
3 |
1 2
|
syl |
|- ( ( Ord A /\ B e. A ) -> ( x e. B -> x C_ B ) ) |
4 |
|
eloni |
|- ( B e. On -> Ord B ) |
5 |
|
ordirr |
|- ( Ord B -> -. B e. B ) |
6 |
4 5
|
syl |
|- ( B e. On -> -. B e. B ) |
7 |
|
eldif |
|- ( B e. ( A \ B ) <-> ( B e. A /\ -. B e. B ) ) |
8 |
7
|
simplbi2 |
|- ( B e. A -> ( -. B e. B -> B e. ( A \ B ) ) ) |
9 |
6 8
|
syl5 |
|- ( B e. A -> ( B e. On -> B e. ( A \ B ) ) ) |
10 |
9
|
adantl |
|- ( ( Ord A /\ B e. A ) -> ( B e. On -> B e. ( A \ B ) ) ) |
11 |
1 10
|
mpd |
|- ( ( Ord A /\ B e. A ) -> B e. ( A \ B ) ) |
12 |
3 11
|
jctild |
|- ( ( Ord A /\ B e. A ) -> ( x e. B -> ( B e. ( A \ B ) /\ x C_ B ) ) ) |
13 |
12
|
adantr |
|- ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( x e. B -> ( B e. ( A \ B ) /\ x C_ B ) ) ) |
14 |
|
sseq2 |
|- ( y = B -> ( x C_ y <-> x C_ B ) ) |
15 |
14
|
rspcev |
|- ( ( B e. ( A \ B ) /\ x C_ B ) -> E. y e. ( A \ B ) x C_ y ) |
16 |
13 15
|
syl6 |
|- ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( x e. B -> E. y e. ( A \ B ) x C_ y ) ) |
17 |
|
eldif |
|- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) ) |
18 |
17
|
biimpri |
|- ( ( x e. A /\ -. x e. B ) -> x e. ( A \ B ) ) |
19 |
|
ssid |
|- x C_ x |
20 |
18 19
|
jctir |
|- ( ( x e. A /\ -. x e. B ) -> ( x e. ( A \ B ) /\ x C_ x ) ) |
21 |
20
|
ex |
|- ( x e. A -> ( -. x e. B -> ( x e. ( A \ B ) /\ x C_ x ) ) ) |
22 |
|
sseq2 |
|- ( y = x -> ( x C_ y <-> x C_ x ) ) |
23 |
22
|
rspcev |
|- ( ( x e. ( A \ B ) /\ x C_ x ) -> E. y e. ( A \ B ) x C_ y ) |
24 |
21 23
|
syl6 |
|- ( x e. A -> ( -. x e. B -> E. y e. ( A \ B ) x C_ y ) ) |
25 |
24
|
adantl |
|- ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> ( -. x e. B -> E. y e. ( A \ B ) x C_ y ) ) |
26 |
16 25
|
pm2.61d |
|- ( ( ( Ord A /\ B e. A ) /\ x e. A ) -> E. y e. ( A \ B ) x C_ y ) |
27 |
26
|
ralrimiva |
|- ( ( Ord A /\ B e. A ) -> A. x e. A E. y e. ( A \ B ) x C_ y ) |
28 |
|
unidif |
|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A ) |
29 |
27 28
|
syl |
|- ( ( Ord A /\ B e. A ) -> U. ( A \ B ) = U. A ) |