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∈ℕ0I|h-1ℕ∈Fin
evlselvlem.e ⊢E=g∈ℕ0J|g-1ℕ∈Fin
evlselvlem.c ⊢C=f∈ℕ0I∖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 ontoD

Proof

Step Hyp Ref Expression
1 evlselvlem.d ⊢D=h∈ℕ0I|h-1ℕ∈Fin
2 evlselvlem.e ⊢E=g∈ℕ0J|g-1ℕ∈Fin
3 evlselvlem.c ⊢C=f∈ℕ0I∖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→finSupp0⁡c
24 23 ad2antrl ⊢φ∧c∈C∧e∈E→finSupp0⁡c
25 2 psrbagfsupp ⊢e∈E→finSupp0⁡e
26 25 ad2antll ⊢φ∧c∈C∧e∈E→finSupp0⁡e
27 24 26 fsuppun ⊢φ∧c∈C∧e∈E→c∪esupp0∈Fin
28 20 21 22 27 isfsuppd ⊢φ∧c∈C∧e∈E→finSupp0⁡c∪e
29 fcdmnn0fsuppg ⊢c∪e∈V∧c∪e:I∖J∪J⟶ℕ0→finSupp0⁡c∪e↔c∪e-1ℕ∈Fin
30 20 13 29 syl2anc ⊢φ∧c∈C∧e∈E→finSupp0⁡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→cFnI∖J
56 10 ffnd ⊢φ∧c∈C∧e∈E→eFnJ
57 fnunres1 ⊢cFnI∖J∧eFnJ∧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 ⊢cFnI∖J∧eFnJ∧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 ontoD