Metamath Proof Explorer

Theorem afv2orxorb

Description: If a set is in the range of a function, the alternate function value at a class A equals this set or is not in the range of the function iff the alternate function value at the class A either equals this set or is not in the range of the function. If B e/ ran F , both disjuncts of the exclusive or can be true: ( F '''' A ) = B -> ( F '''' A ) e/ ran F . (Contributed by AV, 11-Sep-2022)

Ref Expression
Assertion afv2orxorb 
|- ( B e. ran F -> ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) <-> ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( B = ( F '''' A ) -> ( B e. ran F <-> ( F '''' A ) e. ran F ) )
2 1 eqcoms 
 |-  ( ( F '''' A ) = B -> ( B e. ran F <-> ( F '''' A ) e. ran F ) )
3 2 biimpa 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> ( F '''' A ) e. ran F )
4 nnel 
 |-  ( -. ( F '''' A ) e/ ran F <-> ( F '''' A ) e. ran F )
5 3 4 sylibr 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> -. ( F '''' A ) e/ ran F )
6 5 a1d 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) )
7 simpl 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> ( F '''' A ) = B )
8 7 a1d 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) )
9 6 8 jca 
 |-  ( ( ( F '''' A ) = B /\ B e. ran F ) -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) )
10 9 ex 
 |-  ( ( F '''' A ) = B -> ( B e. ran F -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) ) )
11 eleq1 
 |-  ( ( F '''' A ) = B -> ( ( F '''' A ) e. ran F <-> B e. ran F ) )
12 11 anbi2d 
 |-  ( ( F '''' A ) = B -> ( ( ( F '''' A ) e/ ran F /\ ( F '''' A ) e. ran F ) <-> ( ( F '''' A ) e/ ran F /\ B e. ran F ) ) )
13 elnelall 
 |-  ( ( F '''' A ) e. ran F -> ( ( F '''' A ) e/ ran F -> -. ( F '''' A ) e/ ran F ) )
14 13 impcom 
 |-  ( ( ( F '''' A ) e/ ran F /\ ( F '''' A ) e. ran F ) -> -. ( F '''' A ) e/ ran F )
15 12 14 syl6bir 
 |-  ( ( F '''' A ) = B -> ( ( ( F '''' A ) e/ ran F /\ B e. ran F ) -> -. ( F '''' A ) e/ ran F ) )
16 15 com12 
 |-  ( ( ( F '''' A ) e/ ran F /\ B e. ran F ) -> ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) )
17 pm2.24 
 |-  ( ( F '''' A ) e/ ran F -> ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) )
18 17 adantr 
 |-  ( ( ( F '''' A ) e/ ran F /\ B e. ran F ) -> ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) )
19 16 18 jca 
 |-  ( ( ( F '''' A ) e/ ran F /\ B e. ran F ) -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) )
20 19 ex 
 |-  ( ( F '''' A ) e/ ran F -> ( B e. ran F -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) ) )
21 10 20 jaoi 
 |-  ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) -> ( B e. ran F -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) ) )
22 21 com12 
 |-  ( B e. ran F -> ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) -> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) ) )
23 df-xor 
 |-  ( ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) <-> -. ( ( F '''' A ) = B <-> ( F '''' A ) e/ ran F ) )
24 xor3 
 |-  ( -. ( ( F '''' A ) = B <-> ( F '''' A ) e/ ran F ) <-> ( ( F '''' A ) = B <-> -. ( F '''' A ) e/ ran F ) )
25 dfbi2 
 |-  ( ( ( F '''' A ) = B <-> -. ( F '''' A ) e/ ran F ) <-> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) )
26 23 24 25 3bitri 
 |-  ( ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) <-> ( ( ( F '''' A ) = B -> -. ( F '''' A ) e/ ran F ) /\ ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = B ) ) )
27 22 26 syl6ibr 
 |-  ( B e. ran F -> ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) -> ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) ) )
28 xoror 
 |-  ( ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) -> ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) )
29 27 28 impbid1 
 |-  ( B e. ran F -> ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F ) <-> ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) ) )