mapfien2

Description: Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

	Ref	Expression
Hypotheses	mapfien2.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 0 }
	mapfien2.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
	mapfien2.ac	⊢ ( 𝜑 → 𝐴 ≈ 𝐶 )
	mapfien2.bd	⊢ ( 𝜑 → 𝐵 ≈ 𝐷 )
	mapfien2.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
	mapfien2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐷 )
Assertion	mapfien2	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		mapfien2.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 0 }
2		mapfien2.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
3		mapfien2.ac	⊢ ( 𝜑 → 𝐴 ≈ 𝐶 )
4		mapfien2.bd	⊢ ( 𝜑 → 𝐵 ≈ 𝐷 )
5		mapfien2.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
6		mapfien2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐷 )
7		enfixsn	⊢ ( ( 0 ∈ 𝐵 ∧ 𝑊 ∈ 𝐷 ∧ 𝐵 ≈ 𝐷 ) → ∃ 𝑦 ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) )
8	5 6 4 7	syl3anc	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) )
9		bren	⊢ ( 𝐴 ≈ 𝐶 ↔ ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝐶 )
10	3 9	sylib	⊢ ( 𝜑 → ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝐶 )
11		eqid	⊢ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) }
12		eqid	⊢ ( 𝑦 ‘ 0 ) = ( 𝑦 ‘ 0 )
13		f1ocnv	⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝐶 → ^◡ 𝑧 : 𝐶 –1-1-onto→ 𝐴 )
14	13	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ^◡ 𝑧 : 𝐶 –1-1-onto→ 𝐴 )
15		simp3	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝑦 : 𝐵 –1-1-onto→ 𝐷 )
16	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐴 ≈ 𝐶 )
17		relen	⊢ Rel ≈
18	17	brrelex1i	⊢ ( 𝐴 ≈ 𝐶 → 𝐴 ∈ V )
19	16 18	syl	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐴 ∈ V )
20	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐵 ≈ 𝐷 )
21	17	brrelex1i	⊢ ( 𝐵 ≈ 𝐷 → 𝐵 ∈ V )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐵 ∈ V )
23	17	brrelex2i	⊢ ( 𝐴 ≈ 𝐶 → 𝐶 ∈ V )
24	16 23	syl	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐶 ∈ V )
25	17	brrelex2i	⊢ ( 𝐵 ≈ 𝐷 → 𝐷 ∈ V )
26	20 25	syl	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝐷 ∈ V )
27	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 0 ∈ 𝐵 )
28	1 11 12 14 15 19 22 24 26 27	mapfien	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑤 ∈ 𝑆 ↦ ( 𝑦 ∘ ( 𝑤 ∘ ^◡ 𝑧 ) ) ) : 𝑆 –1-1-onto→ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } )
29		ovex	⊢ ( 𝐵 ↑_m 𝐴 ) ∈ V
30	1 29	rabex2	⊢ 𝑆 ∈ V
31	30	f1oen	⊢ ( ( 𝑤 ∈ 𝑆 ↦ ( 𝑦 ∘ ( 𝑤 ∘ ^◡ 𝑧 ) ) ) : 𝑆 –1-1-onto→ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } → 𝑆 ≈ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } )
32	28 31	syl	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → 𝑆 ≈ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } )
33	32	3adant3r	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) ) → 𝑆 ≈ { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } )
34		breq2	⊢ ( ( 𝑦 ‘ 0 ) = 𝑊 → ( 𝑥 finSupp ( 𝑦 ‘ 0 ) ↔ 𝑥 finSupp 𝑊 ) )
35	34	rabbidv	⊢ ( ( 𝑦 ‘ 0 ) = 𝑊 → { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } )
36	35 2	eqtr4di	⊢ ( ( 𝑦 ‘ 0 ) = 𝑊 → { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } = 𝑇 )
37	36	adantl	⊢ ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) → { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } = 𝑇 )
38	37	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) ) → { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp ( 𝑦 ‘ 0 ) } = 𝑇 )
39	33 38	breqtrd	⊢ ( ( 𝜑 ∧ 𝑧 : 𝐴 –1-1-onto→ 𝐶 ∧ ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) ) → 𝑆 ≈ 𝑇 )
40	39	3exp	⊢ ( 𝜑 → ( 𝑧 : 𝐴 –1-1-onto→ 𝐶 → ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) → 𝑆 ≈ 𝑇 ) ) )
41	40	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝐶 → ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) → 𝑆 ≈ 𝑇 ) ) )
42	10 41	mpd	⊢ ( 𝜑 → ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) → 𝑆 ≈ 𝑇 ) )
43	42	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ ( 𝑦 ‘ 0 ) = 𝑊 ) → 𝑆 ≈ 𝑇 ) )
44	8 43	mpd	⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )

Metamath Proof Explorer

Theorem mapfien2

Proof