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 undif ⊢ ( { 𝑋 , 𝑌 } ⊆ 𝐴 ↔ ( { 𝑋 , 𝑌 } ∪ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) = 𝐴 )
9 uncom ⊢ ( { 𝑋 , 𝑌 } ∪ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) = ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } )
10 9 eqeq1i ⊢ ( ( { 𝑋 , 𝑌 } ∪ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) = 𝐴 ↔ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 )
11 8 10 bitri ⊢ ( { 𝑋 , 𝑌 } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 )
12 7 11 sylib ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 )
13 f1oeq23 ⊢ ( ( ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 ∧ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) = 𝐴 ) → ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) ↔ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) )
14 12 12 13 syl2anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) –1-1-onto→ ( ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ∪ { 𝑋 , 𝑌 } ) ↔ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) )
15 6 14 mpbid ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 )
16 f1oco ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) : 𝐴 –1-1-onto→ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
17 15 16 sylan2 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
18 17 3impb ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 )
19 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐴 )
20 coundi ⊢ ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) )
21 fcoconst ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) )
22 21 3adant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) )
23 xpsng ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑋 } × { 𝑌 } ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
24 23 coeq2d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
25 24 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑋 } × { 𝑌 } ) ) = ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
26 fvex ⊢ ( 𝐹 ‘ 𝑌 ) ∈ V
27 xpsng ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) ∈ V ) → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
28 26 27 mpan2 ⊢ ( 𝑋 ∈ 𝐴 → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
29 28 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑋 } × { ( 𝐹 ‘ 𝑌 ) } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
30 22 25 29 3eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } )
31 fcoconst ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) )
32 31 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) )
33 xpsng ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
34 33 coeq2d ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
35 34 ancoms ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
36 35 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 𝑌 } × { 𝑋 } ) ) = ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
37 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
38 xpsng ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ) → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
39 37 38 mpan2 ⊢ ( 𝑌 ∈ 𝐴 → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
40 39 3ad2ant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( { 𝑌 } × { ( 𝐹 ‘ 𝑋 ) } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
41 32 36 40 3eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) = { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
42 30 41 uneq12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } ∪ { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
43 df-pr ⊢ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } = ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } )
44 43 coeq2i ⊢ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = ( 𝐹 ∘ ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
45 coundi ⊢ ( 𝐹 ∘ ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ { ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
46 44 45 eqtri ⊢ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = ( ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ } ) ∪ ( 𝐹 ∘ { ⟨ 𝑌 , 𝑋 ⟩ } ) )
47 df-pr ⊢ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } = ( { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ } ∪ { ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
48 42 46 47 3eqtr4g ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
49 48 uneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ ( 𝐹 ∘ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
50 20 49 eqtrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
51 coires1 ⊢ ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) )
52 51 uneq1i ⊢ ( ( 𝐹 ∘ ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
53 50 52 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
54 19 53 syl3an1 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
55 54 f1oeq1d ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ∘ ( ( I ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ , ⟨ 𝑌 , 𝑋 ⟩ } ) ) : 𝐴 –1-1-onto→ 𝐵 ↔ ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ 𝐵 ) )
56 18 55 mpbid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 , 𝑌 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ , ⟨ 𝑌 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) : 𝐴 –1-1-onto→ 𝐵 )