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