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

Metamath Proof Explorer

Theorem qliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion qliftel ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
3 qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
4 qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 1 2 3 4 qliftlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
6 1 5 2 fliftel ⊢ ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑅 Er 𝑋 )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9 7 8 erth2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐶 𝑅 𝑥 ↔ [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ) )
10 9 anbi1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ↔ ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
11 10 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑋 ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
12 6 11 bitr4d ⊢ ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ) )