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 ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐵 , 𝐴 ⟩ ) )