Metamath Proof Explorer

Theorem fvf1pr

Description: Values of a one-to-one function between two sets with two elements. Actually, such a function is a bijection. (Contributed by AV, 22-Jul-2025)

Ref Expression
Assertion fvf1pr 
|- ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : { A , B } -1-1-> { X , Y } -> F : { A , B } --> { X , Y } )
2 prid1g 
 |-  ( A e. V -> A e. { A , B } )
3 2 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> A e. { A , B } )
4 ffvelcdm 
 |-  ( ( F : { A , B } --> { X , Y } /\ A e. { A , B } ) -> ( F ` A ) e. { X , Y } )
5 1 3 4 syl2anr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( F ` A ) e. { X , Y } )
6 prid2g 
 |-  ( B e. W -> B e. { A , B } )
7 6 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> B e. { A , B } )
8 ffvelcdm 
 |-  ( ( F : { A , B } --> { X , Y } /\ B e. { A , B } ) -> ( F ` B ) e. { X , Y } )
9 1 7 8 syl2anr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( F ` B ) e. { X , Y } )
10 elpri 
 |-  ( ( F ` A ) e. { X , Y } -> ( ( F ` A ) = X \/ ( F ` A ) = Y ) )
11 elpri 
 |-  ( ( F ` B ) e. { X , Y } -> ( ( F ` B ) = X \/ ( F ` B ) = Y ) )
12 eqtr3 
 |-  ( ( ( F ` A ) = X /\ ( F ` B ) = X ) -> ( F ` A ) = ( F ` B ) )
13 3 7 jca 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A e. { A , B } /\ B e. { A , B } ) )
14 f1veqaeq 
 |-  ( ( F : { A , B } -1-1-> { X , Y } /\ ( A e. { A , B } /\ B e. { A , B } ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )
15 13 14 sylan2 
 |-  ( ( F : { A , B } -1-1-> { X , Y } /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )
16 12 15 syl5 
 |-  ( ( F : { A , B } -1-1-> { X , Y } /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = X ) -> A = B ) )
17 16 ex 
 |-  ( F : { A , B } -1-1-> { X , Y } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = X ) -> A = B ) ) )
18 eqneqall 
 |-  ( A = B -> ( A =/= B -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
19 18 com12 
 |-  ( A =/= B -> ( A = B -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
20 19 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A = B -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
21 20 a1i 
 |-  ( F : { A , B } -1-1-> { X , Y } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A = B -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) ) )
22 17 21 syldd 
 |-  ( F : { A , B } -1-1-> { X , Y } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = X ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) ) )
23 22 impcom 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = X ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
24 olc 
 |-  ( ( ( F ` A ) = Y /\ ( F ` B ) = X ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) )
25 24 a1i 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = Y /\ ( F ` B ) = X ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
26 orc 
 |-  ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) )
27 26 a1i 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
28 eqtr3 
 |-  ( ( ( F ` A ) = Y /\ ( F ` B ) = Y ) -> ( F ` A ) = ( F ` B ) )
29 28 15 syl5 
 |-  ( ( F : { A , B } -1-1-> { X , Y } /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( ( ( F ` A ) = Y /\ ( F ` B ) = Y ) -> A = B ) )
30 29 ex 
 |-  ( F : { A , B } -1-1-> { X , Y } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( F ` A ) = Y /\ ( F ` B ) = Y ) -> A = B ) ) )
31 30 21 syldd 
 |-  ( F : { A , B } -1-1-> { X , Y } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( F ` A ) = Y /\ ( F ` B ) = Y ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) ) )
32 31 impcom 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = Y /\ ( F ` B ) = Y ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
33 23 25 27 32 ccased 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( ( F ` A ) = X \/ ( F ` A ) = Y ) /\ ( ( F ` B ) = X \/ ( F ` B ) = Y ) ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
34 10 11 33 syl2ani 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) e. { X , Y } /\ ( F ` B ) e. { X , Y } ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) ) )
35 5 9 34 mp2and 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ F : { A , B } -1-1-> { X , Y } ) -> ( ( ( F ` A ) = X /\ ( F ` B ) = Y ) \/ ( ( F ` A ) = Y /\ ( F ` B ) = X ) ) )