Metamath Proof Explorer


Theorem uniqsALTV

Description: The union of a quotient set, like uniqs but with a weaker antecedent: only the restricion of R by A needs to be a set, not R itself, see e.g. cnvepima . (Contributed by Peter Mazsa, 20-Jun-2019)

Ref Expression
Assertion uniqsALTV ( ( 𝑅𝐴 ) ∈ 𝑉 ( 𝐴 / 𝑅 ) = ( 𝑅𝐴 ) )

Proof

Step Hyp Ref Expression
1 ecex2 ( ( 𝑅𝐴 ) ∈ 𝑉 → ( 𝑥𝐴 → [ 𝑥 ] 𝑅 ∈ V ) )
2 1 ralrimiv ( ( 𝑅𝐴 ) ∈ 𝑉 → ∀ 𝑥𝐴 [ 𝑥 ] 𝑅 ∈ V )
3 dfiun2g ( ∀ 𝑥𝐴 [ 𝑥 ] 𝑅 ∈ V → 𝑥𝐴 [ 𝑥 ] 𝑅 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = [ 𝑥 ] 𝑅 } )
4 2 3 syl ( ( 𝑅𝐴 ) ∈ 𝑉 𝑥𝐴 [ 𝑥 ] 𝑅 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = [ 𝑥 ] 𝑅 } )
5 4 eqcomd ( ( 𝑅𝐴 ) ∈ 𝑉 { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = [ 𝑥 ] 𝑅 } = 𝑥𝐴 [ 𝑥 ] 𝑅 )
6 df-qs ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = [ 𝑥 ] 𝑅 }
7 6 unieqi ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = [ 𝑥 ] 𝑅 }
8 df-ec [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } )
9 8 a1i ( 𝑥𝐴 → [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } ) )
10 9 iuneq2i 𝑥𝐴 [ 𝑥 ] 𝑅 = 𝑥𝐴 ( 𝑅 “ { 𝑥 } )
11 imaiun ( 𝑅 𝑥𝐴 { 𝑥 } ) = 𝑥𝐴 ( 𝑅 “ { 𝑥 } )
12 iunid 𝑥𝐴 { 𝑥 } = 𝐴
13 12 imaeq2i ( 𝑅 𝑥𝐴 { 𝑥 } ) = ( 𝑅𝐴 )
14 10 11 13 3eqtr2ri ( 𝑅𝐴 ) = 𝑥𝐴 [ 𝑥 ] 𝑅
15 5 7 14 3eqtr4g ( ( 𝑅𝐴 ) ∈ 𝑉 ( 𝐴 / 𝑅 ) = ( 𝑅𝐴 ) )