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 𝐹 = 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) ) )