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 ≀ ( 𝑅 ↾ 𝐴 ) / ≀ ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑥 ] ≀ ( 𝑅 ↾ 𝐴 ) ) )