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 ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐵 = ( 𝐹 '''' 𝐴 ) → ( 𝐵 ∈ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) )
2 1 eqcoms ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( 𝐵 ∈ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) )
3 2 biimpa ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
4 nnel ⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
5 3 4 sylibr ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )
6 5 a1d ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
7 simpl ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 )
8 7 a1d ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
9 6 8 jca ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) )
10 9 ex ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) ) )
11 eleq1 ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝐵 ∈ ran 𝐹 ) )
12 11 anbi2d ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) ↔ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) ) )
13 pm2.24nel ⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
14 13 impcom ⊢ ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )
15 12 14 biimtrrdi ⊢ ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
16 15 com12 ⊢ ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
17 pm2.24 ⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
18 17 adantr ⊢ ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
19 16 18 jca ⊢ ( ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) )
20 19 ex ⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) ) )
21 10 20 jaoi ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) ) )
22 21 com12 ⊢ ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) ) )
23 df-xor ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ¬ ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
24 xor3 ⊢ ( ¬ ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
25 dfbi2 ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) )
26 23 24 25 3bitri ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 → ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ∧ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) )
27 22 26 imbitrrdi ⊢ ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )
28 xoror ⊢ ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
29 27 28 impbid1 ⊢ ( 𝐵 ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = 𝐵 ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( 𝐹 '''' 𝐴 ) = 𝐵 ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )