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𝐵 )