Theorem iunmapsn

Description: The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	iunmapsn.x	⊢ Ⅎ 𝑥 𝜑
	iunmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	iunmapsn.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
	iunmapsn.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
Assertion	iunmapsn	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m { 𝐶 } ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		iunmapsn.x	⊢ Ⅎ 𝑥 𝜑
2		iunmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		iunmapsn.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
4		iunmapsn.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
5	1 2 3	iunmapss	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m { 𝐶 } ) ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) )
7	3	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑊 ) )
8	1 7	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
9		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
10	2 8 9	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
11	10 4	mapsnd	⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
13	6 12	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
14		abid	⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } ↔ ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
15	13 14	sylib	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
16		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
17	16	biimpi	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
18	17	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
19		nfcv	⊢ Ⅎ 𝑥 𝑦
20		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
21	19 20	nfel	⊢ Ⅎ 𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
22		nfv	⊢ Ⅎ 𝑥 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ }
23	1 21 22	nf3an	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
24		rspe	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
25	24	ancoms	⊢ ( ( 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
26		abid	⊢ ( 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } ↔ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } )
27	25 26	sylibr	⊢ ( ( 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ∧ 𝑦 ∈ 𝐵 ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
28	27	adantll	⊢ ( ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) ∧ 𝑦 ∈ 𝐵 ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
29	28	3adant2	⊢ ( ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑓 ∈ { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
30	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑍 )
31	3 30	mapsnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ↑m { 𝐶 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } )
32	31	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } = ( 𝐵 ↑m { 𝐶 } ) )
33	32	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } = ( 𝐵 ↑m { 𝐶 } ) )
34	33	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑓 ∣ ∃ 𝑦 ∈ 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } } = ( 𝐵 ↑m { 𝐶 } ) )
35	29 34	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) )
36	35	3exp	⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) ) )
37	36	3adant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) ) )
38	23 37	reximdai	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) )
39	18 38	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } ) → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) )
40	39	3exp	⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) ) )
41	40	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → ( ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑓 = { ⟨ 𝐶 , 𝑦 ⟩ } → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) ) )
43	15 42	mpd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) )
44		eliun	⊢ ( 𝑓 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m { 𝐶 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑓 ∈ ( 𝐵 ↑m { 𝐶 } ) )
45	43 44	sylibr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) ) → 𝑓 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m { 𝐶 } ) )
46	5 45	eqelssd	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m { 𝐶 } ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m { 𝐶 } ) )