Metamath Proof Explorer

Theorem tposf12

Description: Condition for an injective transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf12 ( Rel 𝐴 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
2 relcnv ⊢ Rel ◡ 𝐴
3 cnvf1o ⊢ ( Rel ◡ 𝐴 → ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1-onto→ ◡ ◡ 𝐴 )
4 f1of1 ⊢ ( ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1-onto→ ◡ ◡ 𝐴 → ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴 )
5 2 3 4 mp2b ⊢ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴
6 simpl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → Rel 𝐴 )
7 dfrel2 ⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
8 6 7 sylib ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ ◡ 𝐴 = 𝐴 )
9 f1eq3 ⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
10 8 9 syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
11 5 10 mpbii ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 )
12 f1dm ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → dom 𝐹 = 𝐴 )
13 1 12 syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 = 𝐴 )
14 13 cnveqd ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ dom 𝐹 = ◡ 𝐴 )
15 mpteq1 ⊢ ( ◡ dom 𝐹 = ◡ 𝐴 → ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) )
16 f1eq1 ⊢ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) → ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
17 14 15 16 3syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
18 11 17 mpbird ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 )
19 f1co ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) → ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 )
20 1 18 19 syl2anc ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 )
21 12 releqd ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( Rel dom 𝐹 ↔ Rel 𝐴 ) )
22 21 biimparc ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → Rel dom 𝐹 )
23 dftpos2 ⊢ ( Rel dom 𝐹 → tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) )
24 f1eq1 ⊢ ( tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) → ( tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 ) )
25 22 23 24 3syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 ) )
26 20 25 mpbird ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 )
27 26 ex ⊢ ( Rel 𝐴 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ) )