Theorem iunpw

Description: An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

	Ref	Expression
Hypothesis	iunpw.1	⊢ 𝐴 ∈ V
Assertion	iunpw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		iunpw.1	⊢ 𝐴 ∈ V
2		sseq2	⊢ ( 𝑥 = ∪ 𝐴 → ( 𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ∪ 𝐴 ) )
3	2	biimprcd	⊢ ( 𝑦 ⊆ ∪ 𝐴 → ( 𝑥 = ∪ 𝐴 → 𝑦 ⊆ 𝑥 ) )
4	3	reximdv	⊢ ( 𝑦 ⊆ ∪ 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
5	4	com12	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 → ( 𝑦 ⊆ ∪ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
6		ssiun	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝑥 )
7		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
8	6 7	sseqtrrdi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪ 𝐴 )
9	5 8	impbid1	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 → ( 𝑦 ⊆ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
10		velpw	⊢ ( 𝑦 ∈ 𝒫 ∪ 𝐴 ↔ 𝑦 ⊆ ∪ 𝐴 )
11		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 )
12		velpw	⊢ ( 𝑦 ∈ 𝒫 𝑥 ↔ 𝑦 ⊆ 𝑥 )
13	12	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 )
14	11 13	bitri	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 )
15	9 10 14	3bitr4g	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 → ( 𝑦 ∈ 𝒫 ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ) )
16	15	eqrdv	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 → 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 )
17		ssid	⊢ ∪ 𝐴 ⊆ ∪ 𝐴
18	1	uniex	⊢ ∪ 𝐴 ∈ V
19	18	elpw	⊢ ( ∪ 𝐴 ∈ 𝒫 ∪ 𝐴 ↔ ∪ 𝐴 ⊆ ∪ 𝐴 )
20		eleq2	⊢ ( 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ( ∪ 𝐴 ∈ 𝒫 ∪ 𝐴 ↔ ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ) )
21	19 20	syl5bbr	⊢ ( 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ( ∪ 𝐴 ⊆ ∪ 𝐴 ↔ ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ) )
22	17 21	mpbii	⊢ ( 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 )
23		eliun	⊢ ( ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥 )
24	22 23	sylib	⊢ ( 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥 )
25		elssuni	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
26		elpwi	⊢ ( ∪ 𝐴 ∈ 𝒫 𝑥 → ∪ 𝐴 ⊆ 𝑥 )
27	25 26	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥 ) → ( 𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑥 ) )
28		eqss	⊢ ( 𝑥 = ∪ 𝐴 ↔ ( 𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑥 ) )
29	27 28	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥 ) → 𝑥 = ∪ 𝐴 )
30	29	ex	⊢ ( 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ∈ 𝒫 𝑥 → 𝑥 = ∪ 𝐴 ) )
31	30	reximia	⊢ ( ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥 → ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 )
32	24 31	syl	⊢ ( 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 )
33	16 32	impbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 )