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 ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
evlselvlem.e ⊢ E = g ∈ ℕ 0 J | g -1 ℕ ∈ Fin
evlselvlem.c ⊢ C = f ∈ ℕ 0 I ∖ J | f -1 ℕ ∈ Fin
evlselvlem.h ⊢ H = c ∈ C , e ∈ E ⟼ c ∪ e
evlselvlem.i ⊢ φ → I ∈ V
evlselvlem.j ⊢ φ → J ⊆ I
Assertion evlselvlem ⊢ φ → H : C × E ⟶ 1-1 onto D

Proof

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