Metamath Proof Explorer

Theorem evlselvlem

Description: Lemma for evlselv . Used to re-index to and from bags of variables in I and bags of variables in the subsets J and I \ J . (Contributed by SN, 10-Mar-2025)

Ref Expression
Hypotheses evlselvlem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlselvlem.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
evlselvlem.c ⊢ 𝐶 = { 𝑓 ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
evlselvlem.h ⊢ 𝐻 = ( 𝑐 ∈ 𝐶 , 𝑒 ∈ 𝐸 ↦ ( 𝑐 ∪ 𝑒 ) )
evlselvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlselvlem.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion evlselvlem ( 𝜑 → 𝐻 : ( 𝐶 × 𝐸 ) –1-1-onto→ 𝐷 )

Proof

Step Hyp Ref Expression
1 evlselvlem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 evlselvlem.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
3 evlselvlem.c ⊢ 𝐶 = { 𝑓 ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4 evlselvlem.h ⊢ 𝐻 = ( 𝑐 ∈ 𝐶 , 𝑒 ∈ 𝐸 ↦ ( 𝑐 ∪ 𝑒 ) )
5 evlselvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 evlselvlem.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
7 undifr ⊢ ( 𝐽 ⊆ 𝐼 ↔ ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
8 6 7 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
10 3 psrbagf ⊢ ( 𝑐 ∈ 𝐶 → 𝑐 : ( 𝐼 ∖ 𝐽 ) ⟶ ℕ0 )
11 10 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 : ( 𝐼 ∖ 𝐽 ) ⟶ ℕ0 )
12 2 psrbagf ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 : 𝐽 ⟶ ℕ0 )
13 12 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 : 𝐽 ⟶ ℕ0 )
14 disjdifr ⊢ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅
15 14 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ )
16 11 13 15 fun2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) : ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ⟶ ℕ0 )
17 9 16 feq2dd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 )
18 unexg ⊢ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) → ( 𝑐 ∪ 𝑒 ) ∈ V )
19 18 adantl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) ∈ V )
20 0zd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 0 ∈ ℤ )
21 16 ffund ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → Fun ( 𝑐 ∪ 𝑒 ) )
22 3 psrbagfsupp ⊢ ( 𝑐 ∈ 𝐶 → 𝑐 finSupp 0 )
23 22 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 finSupp 0 )
24 2 psrbagfsupp ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 finSupp 0 )
25 24 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 finSupp 0 )
26 23 25 fsuppun ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) supp 0 ) ∈ Fin )
27 19 20 21 26 isfsuppd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) finSupp 0 )
28 fcdmnn0fsuppg ⊢ ( ( ( 𝑐 ∪ 𝑒 ) ∈ V ∧ ( 𝑐 ∪ 𝑒 ) : ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ⟶ ℕ0 ) → ( ( 𝑐 ∪ 𝑒 ) finSupp 0 ↔ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) )
29 19 16 28 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) finSupp 0 ↔ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) )
30 27 29 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin )
31 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝐼 ∈ 𝑉 )
32 1 psrbag ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 ↔ ( ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) ) )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 ↔ ( ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) ) )
34 17 30 33 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 )
35 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
36 difssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝐼 ∖ 𝐽 ) ⊆ 𝐼 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ 𝐷 )
38 1 3 35 36 37 psrbagres ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∈ 𝐶 )
39 6 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝐽 ⊆ 𝐼 )
40 1 2 35 39 37 psrbagres ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑑 ↾ 𝐽 ) ∈ 𝐸 )
41 1 psrbagf ⊢ ( 𝑑 ∈ 𝐷 → 𝑑 : 𝐼 ⟶ ℕ0 )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 : 𝐼 ⟶ ℕ0 )
43 42 freld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → Rel 𝑑 )
44 42 fdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → dom 𝑑 = 𝐼 )
45 39 7 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
46 44 45 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → dom 𝑑 = ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) )
47 reldmun ⊢ ( ( Rel 𝑑 ∧ dom 𝑑 = ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
48 43 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
49 48 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
50 uneq12 ⊢ ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → ( 𝑐 ∪ 𝑒 ) = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
51 50 eqeq2d ⊢ ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → ( 𝑑 = ( 𝑐 ∪ 𝑒 ) ↔ 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) ) )
52 49 51 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → 𝑑 = ( 𝑐 ∪ 𝑒 ) ) )
53 11 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 Fn ( 𝐼 ∖ 𝐽 ) )
54 13 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 Fn 𝐽 )
55 fnunres1 ⊢ ( ( 𝑐 Fn ( 𝐼 ∖ 𝐽 ) ∧ 𝑒 Fn 𝐽 ∧ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ) → ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) = 𝑐 )
56 53 54 15 55 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) = 𝑐 )
57 56 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) )
58 fnunres2 ⊢ ( ( 𝑐 Fn ( 𝐼 ∖ 𝐽 ) ∧ 𝑒 Fn 𝐽 ∧ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ) → ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) = 𝑒 )
59 53 54 15 58 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) = 𝑒 )
60 59 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) )
61 57 60 jca ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
62 61 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
63 reseq1 ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) )
64 63 eqeq2d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ↔ 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ) )
65 reseq1 ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑑 ↾ 𝐽 ) = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) )
66 65 eqeq2d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑒 = ( 𝑑 ↾ 𝐽 ) ↔ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
67 64 66 anbi12d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ↔ ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) ) )
68 62 67 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ) )
69 52 68 impbid ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ↔ 𝑑 = ( 𝑐 ∪ 𝑒 ) ) )
70 4 34 38 40 69 mpof1o2d ⊢ ( 𝜑 → 𝐻 : ( 𝐶 × 𝐸 ) –1-1-onto→ 𝐷 )