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

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 dfrel2 ⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
7 6 birani ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ ◡ 𝐴 = 𝐴 )
8 f1eq3 ⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
9 7 8 syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ ◡ ◡ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
10 5 9 mpbii ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 )
11 f1dm ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → dom 𝐹 = 𝐴 )
12 1 11 syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 = 𝐴 )
13 12 cnveqd ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ dom 𝐹 = ◡ 𝐴 )
14 mpteq1 ⊢ ( ◡ dom 𝐹 = ◡ 𝐴 → ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) )
15 f1eq1 ⊢ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) → ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
16 13 14 15 3syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ↔ ( 𝑥 ∈ ◡ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) )
17 10 16 mpbird ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 )
18 f1co ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) : ◡ 𝐴 –1-1→ 𝐴 ) → ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 )
19 1 17 18 syl2anc ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 )
20 11 releqd ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( Rel dom 𝐹 ↔ Rel 𝐴 ) )
21 20 biimparc ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → Rel dom 𝐹 )
22 dftpos2 ⊢ ( Rel dom 𝐹 → tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) )
23 f1eq1 ⊢ ( tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) → ( tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 ) )
24 21 22 23 3syl ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) : ◡ 𝐴 –1-1→ 𝐵 ) )
25 19 24 mpbird ⊢ ( ( Rel 𝐴 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 )
26 25 ex ⊢ ( Rel 𝐴 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → tpos 𝐹 : ◡ 𝐴 –1-1→ 𝐵 ) )