Step |
Hyp |
Ref |
Expression |
1 |
|
ipoval.i |
|- I = ( toInc ` F ) |
2 |
|
ipole.l |
|- .<_ = ( le ` I ) |
3 |
|
preq12 |
|- ( ( x = X /\ y = Y ) -> { x , y } = { X , Y } ) |
4 |
3
|
sseq1d |
|- ( ( x = X /\ y = Y ) -> ( { x , y } C_ F <-> { X , Y } C_ F ) ) |
5 |
|
sseq12 |
|- ( ( x = X /\ y = Y ) -> ( x C_ y <-> X C_ Y ) ) |
6 |
4 5
|
anbi12d |
|- ( ( x = X /\ y = Y ) -> ( ( { x , y } C_ F /\ x C_ y ) <-> ( { X , Y } C_ F /\ X C_ Y ) ) ) |
7 |
|
eqid |
|- { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } |
8 |
6 7
|
brabga |
|- ( ( X e. F /\ Y e. F ) -> ( X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) ) |
9 |
8
|
3adant1 |
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) ) |
10 |
1
|
ipolerval |
|- ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) ) |
11 |
2 10
|
eqtr4id |
|- ( F e. V -> .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) |
12 |
11
|
breqd |
|- ( F e. V -> ( X .<_ Y <-> X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y ) ) |
13 |
12
|
3ad2ant1 |
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y ) ) |
14 |
|
prssi |
|- ( ( X e. F /\ Y e. F ) -> { X , Y } C_ F ) |
15 |
14
|
3adant1 |
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> { X , Y } C_ F ) |
16 |
15
|
biantrurd |
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X C_ Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) ) |
17 |
9 13 16
|
3bitr4d |
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X C_ Y ) ) |