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

Metamath Proof Explorer

Theorem f1ofvswap

Description: Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024)

Ref Expression
Assertion f1ofvswap ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 f1oi ⊢ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) : ( 𝐴 ∖ { 𝑋 , 𝑌 } ) –1-1-onto→ ( 𝐴 ∖ { 𝑋 , 𝑌 } )
2 f1oprswap ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } : { 𝑋 , 𝑌 } –1-1-onto→ { 𝑋 , 𝑌 } )
3 disjdifr ⊢ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∩ { 𝑋 , 𝑌 } ) = ∅
4 f1oun ⊢ ( ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) : ( 𝐴 ∖ { 𝑋 , 𝑌 } ) –1-1-onto→ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∧ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } : { 𝑋 , 𝑌 } –1-1-onto→ { 𝑋 , 𝑌 } ) ∧ ( ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∩ { 𝑋 , 𝑌 } ) = ∅ ∧ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∩ { 𝑋 , 𝑌 } ) = ∅ ) ) → ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) )
5 3 3 4 mpanr12 ⊢ ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) : ( 𝐴 ∖ { 𝑋 , 𝑌 } ) –1-1-onto→ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∧ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } : { 𝑋 , 𝑌 } –1-1-onto→ { 𝑋 , 𝑌 } ) → ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) )
6 1 2 5 sylancr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) )
7 prssi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → { 𝑋 , 𝑌 } ⊆ 𝐴 )
8 undifr ⊢ ( { 𝑋 , 𝑌 } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 )
9 7 8 sylib ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 )
10 f1oeq23 ⊢ ( ( ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 ∧ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 ) → ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) ↔ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) )
11 9 9 10 syl2anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) ↔ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) )
12 6 11 mpbid ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 )
13 f1oco ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
14 12 13 sylan2 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
15 14 3impb ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
16 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐴 )
17 coundi ⊢ ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) )
18 fcoconst ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) )
19 18 3adant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) )
20 xpsng ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑋 } × { 𝑌 } ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
21 20 coeq2d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
22 21 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
23 fvex ⊢ ( 𝐹 ‘ 𝑌 ) ∈ V
24 xpsng ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) ∈ V ) → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
25 23 24 mpan2 ⊢ ( 𝑋 ∈ 𝐴 → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
26 25 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
27 19 22 26 3eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
28 fcoconst ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) )
29 28 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) )
30 xpsng ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
31 30 coeq2d ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
32 31 ancoms ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
33 32 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
34 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
35 xpsng ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ) → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
36 34 35 mpan2 ⊢ ( 𝑌 ∈ 𝐴 → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
37 36 3ad2ant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
38 29 33 37 3eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
39 27 38 uneq12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } ∪ { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
40 df-pr ⊢ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } = ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } )
41 40 coeq2i ⊢ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = ( 𝐹 ∘ ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
42 coundi ⊢ ( 𝐹 ∘ ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
43 41 42 eqtri ⊢ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
44 df-pr ⊢ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } = ( { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } ∪ { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
45 39 43 44 3eqtr4g ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
46 45 uneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
47 17 46 eqtrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
48 coires1 ⊢ ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) )
49 48 uneq1i ⊢ ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
50 47 49 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
51 16 50 syl3an1 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
52 51 f1oeq1d ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ 𝐵 ) )
53 15 52 mpbid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ 𝐵 )