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

Metamath Proof Explorer

Theorem uniqs

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

Ref Expression
Assertion uniqs ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elecex ⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝑥 ∈ 𝐴 → [ 𝑥 ] 𝑅 ∈ 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 ⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )