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

Metamath Proof Explorer

Theorem cnvuni

Description: The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004)

		Ref	Expression
	Assertion	cnvuni	⊢ ^◡ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ^◡ 𝑥

Proof

Step	Hyp	Ref	Expression
1		elcnv2	⊢ ( 𝑦 ∈ ^◡ ∪ 𝐴 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ ∪ 𝐴 ) )
2		eluni2	⊢ ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 )
3	2	anbi2i	⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ ∪ 𝐴 ) ↔ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
4		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) ↔ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
5	3 4	bitr4i	⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ ∪ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
6	5	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ ∪ 𝐴 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
7		elcnv2	⊢ ( 𝑦 ∈ ^◡ 𝑥 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
8	7	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ^◡ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
9		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
10		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑤 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
11	10	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ∃ 𝑤 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) )
12	8 9 11	3bitrri	⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∈ 𝐴 ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑤 , 𝑧 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ^◡ 𝑥 )
13	1 6 12	3bitri	⊢ ( 𝑦 ∈ ^◡ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ^◡ 𝑥 )
14		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ^◡ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ^◡ 𝑥 )
15	13 14	bitr4i	⊢ ( 𝑦 ∈ ^◡ ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ^◡ 𝑥 )
16	15	eqriv	⊢ ^◡ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ^◡ 𝑥