Metamath Proof Explorer

Theorem fcoinvbr

Description: Binary relation for the equivalence relation from fcoinver . (Contributed by Thierry Arnoux, 3-Jan-2020)

Ref Expression
Hypothesis fcoinvbr.e ⊢ ∼ = ( ◡ 𝐹 ∘ 𝐹 )
Assertion fcoinvbr ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 fcoinvbr.e ⊢ ∼ = ( ◡ 𝐹 ∘ 𝐹 )
2 1 breqi ⊢ ( 𝑋 ∼ 𝑌 ↔ 𝑋 ( ◡ 𝐹 ∘ 𝐹 ) 𝑌 )
3 brcog ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ( ◡ 𝐹 ∘ 𝐹 ) 𝑌 ↔ ∃ 𝑧 ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
4 2 3 syl5bb ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∼ 𝑌 ↔ ∃ 𝑧 ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
5 4 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∼ 𝑌 ↔ ∃ 𝑧 ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
6 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
7 6 eqvinc ⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑋 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑌 ) ) )
8 eqcom ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑧 )
9 eqcom ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) = 𝑧 )
10 8 9 anbi12i ⊢ ( ( 𝑧 = ( 𝐹 ‘ 𝑋 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) )
11 10 exbii ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑋 ) ∧ 𝑧 = ( 𝐹 ‘ 𝑌 ) ) ↔ ∃ 𝑧 ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) )
12 7 11 bitri ⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ ∃ 𝑧 ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) )
13 fnbrfvb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ↔ 𝑋 𝐹 𝑧 ) )
14 13 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ↔ 𝑋 𝐹 𝑧 ) )
15 fnbrfvb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑌 ) = 𝑧 ↔ 𝑌 𝐹 𝑧 ) )
16 15 3adant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑌 ) = 𝑧 ↔ 𝑌 𝐹 𝑧 ) )
17 14 16 anbi12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) ↔ ( 𝑋 𝐹 𝑧 ∧ 𝑌 𝐹 𝑧 ) ) )
18 vex ⊢ 𝑧 ∈ V
19 brcnvg ⊢ ( ( 𝑧 ∈ V ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ◡ 𝐹 𝑌 ↔ 𝑌 𝐹 𝑧 ) )
20 18 19 mpan ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑧 ◡ 𝐹 𝑌 ↔ 𝑌 𝐹 𝑧 ) )
21 20 3ad2ant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ◡ 𝐹 𝑌 ↔ 𝑌 𝐹 𝑧 ) )
22 21 anbi2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ↔ ( 𝑋 𝐹 𝑧 ∧ 𝑌 𝐹 𝑧 ) ) )
23 17 22 bitr4d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) ↔ ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
24 23 exbidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ∃ 𝑧 ( ( 𝐹 ‘ 𝑋 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑌 ) = 𝑧 ) ↔ ∃ 𝑧 ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
25 12 24 syl5bb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ ∃ 𝑧 ( 𝑋 𝐹 𝑧 ∧ 𝑧 ◡ 𝐹 𝑌 ) ) )
26 5 25 bitr4d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )