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

Metamath Proof Explorer

Theorem fliftcnv

Description: Converse of the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion fliftcnv ( 𝜑 → ◡ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2 flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3 flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4 eqid ⊢ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ )
5 4 3 2 fliftrel ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ⊆ ( 𝑆 × 𝑅 ) )
6 relxp ⊢ Rel ( 𝑆 × 𝑅 )
7 relss ⊢ ( ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ⊆ ( 𝑆 × 𝑅 ) → ( Rel ( 𝑆 × 𝑅 ) → Rel ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ) )
8 5 6 7 mpisyl ⊢ ( 𝜑 → Rel ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )
9 relcnv ⊢ Rel ◡ 𝐹
10 8 9 jctil ⊢ ( 𝜑 → ( Rel ◡ 𝐹 ∧ Rel ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ) )
11 1 2 3 fliftel ⊢ ( 𝜑 → ( 𝑧 𝐹 𝑦 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
12 vex ⊢ 𝑦 ∈ V
13 vex ⊢ 𝑧 ∈ V
14 12 13 brcnv ⊢ ( 𝑦 ◡ 𝐹 𝑧 ↔ 𝑧 𝐹 𝑦 )
15 ancom ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐴 ) ↔ ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) )
16 15 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) )
17 11 14 16 3bitr4g ⊢ ( 𝜑 → ( 𝑦 ◡ 𝐹 𝑧 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐴 ) ) )
18 4 3 2 fliftel ⊢ ( 𝜑 → ( 𝑦 ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) 𝑧 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐴 ) ) )
19 17 18 bitr4d ⊢ ( 𝜑 → ( 𝑦 ◡ 𝐹 𝑧 ↔ 𝑦 ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) 𝑧 ) )
20 df-br ⊢ ( 𝑦 ◡ 𝐹 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐹 )
21 df-br ⊢ ( 𝑦 ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )
22 19 20 21 3bitr3g ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ) )
23 22 eqrelrdv2 ⊢ ( ( ( Rel ◡ 𝐹 ∧ Rel ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) ) ∧ 𝜑 ) → ◡ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )
24 10 23 mpancom ⊢ ( 𝜑 → ◡ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )