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

Metamath Proof Explorer

Theorem eldmqs1cossres

Description: Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019)

Ref Expression
Assertion eldmqs1cossres ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ≀ ( 𝑅 ↾ 𝐴 ) / ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elqsg ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ≀ ( 𝑅 ↾ 𝐴 ) / ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
2 df-rex ⊢ ( ∃ 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
3 eldm1cossres2 ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ) )
4 3 elv ⊢ ( 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 )
5 4 anbi1i ⊢ ( ( 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
6 5 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
7 2 6 bitri ⊢ ( ∃ 𝑥 ∈ dom ≀ ( 𝑅 ↾ 𝐴 ) 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
8 1 7 bitrdi ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ≀ ( 𝑅 ↾ 𝐴 ) / ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ) )
9 df-rex ⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
10 9 rexbii ⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
11 rexcom4 ⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
12 r19.41v ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
13 12 exbii ⊢ ( ∃ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
14 11 13 bitri ⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
15 10 14 bitri ⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )
16 8 15 bitr4di ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( dom ≀ ( 𝑅 ↾ 𝐴 ) / ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )