This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → 𝐹 : { 𝐴 , 𝐵 } ⟶ { 𝑋 , 𝑌 } )
2 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
4 ffvelcdm ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ { 𝑋 , 𝑌 } ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐴 ) ∈ { 𝑋 , 𝑌 } )
5 1 3 4 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( 𝐹 ‘ 𝐴 ) ∈ { 𝑋 , 𝑌 } )
6 prid2g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
7 6 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
8 ffvelcdm ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ { 𝑋 , 𝑌 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐵 ) ∈ { 𝑋 , 𝑌 } )
9 1 7 8 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( 𝐹 ‘ 𝐵 ) ∈ { 𝑋 , 𝑌 } )
10 elpri ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ { 𝑋 , 𝑌 } → ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∨ ( 𝐹 ‘ 𝐴 ) = 𝑌 ) )
11 elpri ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ { 𝑋 , 𝑌 } → ( ( 𝐹 ‘ 𝐵 ) = 𝑋 ∨ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) )
12 eqtr3 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
13 3 7 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) )
14 f1veqaeq ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
15 13 14 sylan2 ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
16 12 15 syl5 ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → 𝐴 = 𝐵 ) )
17 16 ex ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → 𝐴 = 𝐵 ) ) )
18 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
19 18 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐴 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
20 19 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
21 20 a1i ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) ) )
22 17 21 syldd ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) ) )
23 22 impcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
24 olc ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) )
25 24 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
26 orc ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) )
27 26 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
28 eqtr3 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
29 28 15 syl5 ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → 𝐴 = 𝐵 ) )
30 29 ex ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → 𝐴 = 𝐵 ) ) )
31 30 21 syldd ⊢ ( 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) ) )
32 31 impcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
33 23 25 27 32 ccased ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∨ ( 𝐹 ‘ 𝐴 ) = 𝑌 ) ∧ ( ( 𝐹 ‘ 𝐵 ) = 𝑋 ∨ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
34 10 11 33 syl2ani ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ { 𝑋 , 𝑌 } ∧ ( 𝐹 ‘ 𝐵 ) ∈ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) ) )
35 5 9 34 mp2and ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐹 : { 𝐴 , 𝐵 } –1-1→ { 𝑋 , 𝑌 } ) → ( ( ( 𝐹 ‘ 𝐴 ) = 𝑋 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑌 ) ∨ ( ( 𝐹 ‘ 𝐴 ) = 𝑌 ∧ ( 𝐹 ‘ 𝐵 ) = 𝑋 ) ) )