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

Metamath Proof Explorer

Theorem tpossym

Description: Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion tpossym ( 𝐹 Fn ( 𝐴 × 𝐴 ) → ( tpos 𝐹 = 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 tposfn ⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → tpos 𝐹 Fn ( 𝐴 × 𝐴 ) )
2 eqfnov2 ⊢ ( ( tpos 𝐹 Fn ( 𝐴 × 𝐴 ) ∧ 𝐹 Fn ( 𝐴 × 𝐴 ) ) → ( tpos 𝐹 = 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑦 ) ) )
3 1 2 mpancom ⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → ( tpos 𝐹 = 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑦 ) ) )
4 eqcom ⊢ ( ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 𝐹 𝑦 ) = ( 𝑥 tpos 𝐹 𝑦 ) )
5 ovtpos ⊢ ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
6 5 eqeq2i ⊢ ( ( 𝑥 𝐹 𝑦 ) = ( 𝑥 tpos 𝐹 𝑦 ) ↔ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) )
7 4 6 bitri ⊢ ( ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) )
8 7 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 tpos 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) )
9 3 8 bitrdi ⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → ( tpos 𝐹 = 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) )